From f5461eb3d4eb2605b546a4ed202c12bcdaa1f4e4 Mon Sep 17 00:00:00 2001 From: "john.j.camilleri" Date: Mon, 16 Sep 2013 07:17:27 +0000 Subject: Remove contribs and examples Everything has now been moved to a separate repository at https://github.com/GrammaticalFramework/gf-contrib The contents of the examples folder are build during SetupWeb --- examples/category-theory/InitialAndTerminal.gf | 46 -------------------------- 1 file changed, 46 deletions(-) delete mode 100644 examples/category-theory/InitialAndTerminal.gf (limited to 'examples/category-theory/InitialAndTerminal.gf') diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf deleted file mode 100644 index b8a9f00c9..000000000 --- a/examples/category-theory/InitialAndTerminal.gf +++ /dev/null @@ -1,46 +0,0 @@ -abstract InitialAndTerminal = Morphisms ** { - -cat Initial ({c} : Category) (Obj c) ; -data initial : ({c} : Category) - -> (x : Obj c) - -> ((y : Obj c) -> Arrow x y) - -> Initial x ; - -fun initAr : ({c} : Category) - -> ({x} : Obj c) - -> Initial x - -> (y : Obj c) - -> Arrow x y ; --- def initAr {~c} {~x} (initial {c} x f) y = f y ; -{- -fun initials2iso : ({c} : Category) - -> ({x,y} : Obj c) - -> (ix : Initial x) - -> (iy : Initial y) - -> Iso (initAr ix y) (initAr iy x) ; --} --- def initials2iso = .. ; - - -cat Terminal ({c} : Category) (Obj c) ; -data terminal : ({c} : Category) - -> (y : Obj c) - -> ((x : Obj c) -> Arrow x y) - -> Terminal y ; - -fun terminalAr : ({c} : Category) - -> (x : Obj c) - -> ({y} : Obj c) - -> Terminal y - -> Arrow x y ; --- def terminalAr {c} x {~y} (terminal {~c} y f) = f x ; -{- -fun terminals2iso : ({c} : Category) - -> ({x,y} : Obj c) - -> (tx : Terminal x) - -> (ty : Terminal y) - -> Iso (terminalAr x ty) (terminalAr y tx) ; - -} --- def terminals2iso = .. ; - -} -- cgit v1.2.3