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/Adjoints.gf | 16 -- examples/category-theory/Categories.gf | 201 ------------------------- examples/category-theory/CategoryTheory.gf | 11 -- examples/category-theory/Equalizer.gf | 49 ------ examples/category-theory/Functor.gf | 53 ------- examples/category-theory/InitialAndTerminal.gf | 46 ------ examples/category-theory/Monad.gf | 30 ---- examples/category-theory/Morphisms.gf | 92 ----------- examples/category-theory/NaturalTransform.gf | 19 --- 9 files changed, 517 deletions(-) delete mode 100644 examples/category-theory/Adjoints.gf delete mode 100644 examples/category-theory/Categories.gf delete mode 100644 examples/category-theory/CategoryTheory.gf delete mode 100644 examples/category-theory/Equalizer.gf delete mode 100644 examples/category-theory/Functor.gf delete mode 100644 examples/category-theory/InitialAndTerminal.gf delete mode 100644 examples/category-theory/Monad.gf delete mode 100644 examples/category-theory/Morphisms.gf delete mode 100644 examples/category-theory/NaturalTransform.gf (limited to 'examples/category-theory') diff --git a/examples/category-theory/Adjoints.gf b/examples/category-theory/Adjoints.gf deleted file mode 100644 index b4987228d..000000000 --- a/examples/category-theory/Adjoints.gf +++ /dev/null @@ -1,16 +0,0 @@ -abstract Adjoints = NaturalTransform ** { - - ---------------------------------------------------------- - -- Adjoint functors - pair of functors such that - -- there is a natural transformation from the identity - -- functor to the composition of the functors. - - cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ; - - data adjoints : ({c1,c2} : Category) - -> (f : Functor c1 c2) - -> (g : Functor c2 c1) - -> NT (idF c1) (compF g f) - -> Adjoints f g ; - -} diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf deleted file mode 100644 index b20dccde9..000000000 --- a/examples/category-theory/Categories.gf +++ /dev/null @@ -1,201 +0,0 @@ -abstract Categories = { - - ------------------------------------------------------- - -- Basic category theory: categories, objects, - -- arrows and equality of arrows - - cat Category ; - Obj Category ; - Arrow ({c} : Category) (Obj c) (Obj c) ; - EqAr ({c} : Category) ({x,y} : Obj c) (f,g : Arrow x y) ; - - fun dom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ; - def dom {_} {x} {y} _ = x ; - - fun codom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ; - def codom {_} {x} {y} _ = y ; - - -- 'id x' is the identity arrow for object x - fun id : ({c} : Category) -> (x : Obj c) -> Arrow x x ; - - -- composition of arrows - fun comp : ({c} : Category) -> ({x,y,z} : Obj c) -> Arrow z y -> Arrow x z -> Arrow x y ; - - - ------------------------------------------------------- - -- The basic equality properties: reflexive, - -- symetric and transitive relation. - -- Only the reflexivity is an axiom. - - data eqRefl : ({c} : Category) - -> ({x,y} : Obj c) - -> (a : Arrow x y) - -> EqAr a a ; - - fun eqSym : ({c} : Category) - -> ({x,y} : Obj c) - -> ({a,b} : Arrow x y) - -> EqAr a b - -> EqAr b a ; - def eqSym (eqRefl a) = eqRefl a ; - - fun eqTran : ({c} : Category) - -> ({x,y} : Obj c) - -> ({f,g,h} : Arrow x y) - -> EqAr f g - -> EqAr f h - -> EqAr g h ; - def eqTran (eqRefl a) eq = eq ; - - - ------------------------------------------------------- - -- Now we prove some theorems which are specific for - -- the equality of arrows - -- - -- First we assert the axioms: - -- - -- a . id == id . a == a - -- f . (g . h) == (f . g) . h - -- - -- and after that we prove that the composition - -- preserves the equality. - - fun eqIdL : ({c} : Category) - -> ({x,y} : Obj c) - -> (a : Arrow x y) - -> EqAr (comp a (id x)) a ; - eqIdR : ({c} : Category) - -> ({x,y} : Obj c) - -> (a : Arrow x y) - -> EqAr (comp (id y) a) a ; - - fun eqAssoc : ({c} : Category) - -> ({w,x,y,z} : Obj c) - -> (f : Arrow w y) - -> (g : Arrow z w) - -> (h : Arrow x z) - -> EqAr (comp f (comp g h)) (comp (comp f g) h) ; - - fun eqCompL : ({c} : Category) - -> ({x,y,z} : Obj c) - -> ({g,h} : Arrow x z) - -> (f : Arrow z y) - -> EqAr g h - -> EqAr (comp f g) (comp f h) ; - def eqCompL f (eqRefl g) = eqRefl (comp f g) ; - - fun eqCompR : ({c} : Category) - -> ({x,y,z} : Obj c) - -> ({g,h} : Arrow z y) - -> EqAr g h - -> (f : Arrow x z) - -> EqAr (comp g f) (comp h f) ; - def eqCompR (eqRefl g) f = eqRefl (comp g f) ; - - - ------------------------------------------------------- - -- Operations over categories - -- - - -- 1. Dual category - data Op : (c : Category) - -> Category ; - opObj: ({c} : Category) - -> (x : Obj c) - -> Obj (Op c) ; - opAr : ({c} : Category) - -> ({x,y} : Obj c) - -> (a : Arrow x y) - -> Arrow {Op c} (opObj y) (opObj x) ; - def id (opObj x) = opAr (id x) ; - def comp (opAr f) (opAr g) = opAr (comp g f) ; - - fun eqOp : ({c} : Category) - -> ({x,y} : Obj c) - -> ({f} : Arrow x y) - -> ({g} : Arrow x y) - -> EqAr f g - -> EqAr (opAr f) (opAr g) ; - def eqOp (eqRefl f) = eqRefl (opAr f) ; - - -- 2. Slash of a category - data Slash : (c : Category) - -> (x : Obj c) - -> Category ; - slashObj : ({c} : Category) - -> (x,{y} : Obj c) - -> Arrow y x - -> Obj (Slash c x) ; - slashAr : ({c} : Category) - -> (x,{y,z} : Obj c) - -> ({ay} : Arrow y x) - -> ({az} : Arrow z x) - -> Arrow y z - -> Arrow (slashObj x ay) (slashObj x az) ; - def id (slashObj x {y} a) = slashAr x (id y) ; - def comp (slashAr t azy) (slashAr ~t axz) = slashAr t (comp azy axz) ; - - -- 3. CoSlash of a category - data CoSlash : (c : Category) - -> (x : Obj c) - -> Category ; - coslashObj: ({c} : Category) - -> (x,{y} : Obj c) - -> Arrow x y - -> Obj (CoSlash c x) ; - coslashAr : ({c} : Category) - -> (x,{y,z} : Obj c) - -> ({ay} : Arrow x y) - -> ({az} : Arrow x z) - -> Arrow z y - -> Arrow (coslashObj x ay) (coslashObj x az) ; - def id (coslashObj x {y} a) = coslashAr x (id y) ; - def comp (coslashAr t ayz) (coslashAr ~t azx) = coslashAr t (comp azx ayz) ; - - -- 4. Cartesian product of two categories - data Prod : (c1,c2 : Category) - -> Category ; - prodObj: ({c1,c2} : Category) - -> Obj c1 - -> Obj c2 - -> Obj (Prod c1 c2) ; - prodAr : ({c1,c2} : Category) - -> ({x1,y1} : Obj c1) - -> ({x2,y2} : Obj c2) - -> Arrow x1 y1 - -> Arrow x2 y2 - -> Arrow (prodObj x1 x2) (prodObj y1 y2) ; - def id (prodObj x1 x2) = prodAr (id x1) (id x2) ; - def comp (prodAr f1 f2) (prodAr g1 g2) = prodAr (comp f1 g1) (comp f2 g2) ; - - fun fst : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c1 ; - def fst (prodObj x1 _) = x1 ; - - fun snd : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c2 ; - def snd (prodObj _ x2) = x2 ; - - -- 5. Sum of two categories - data Sum : (c1,c2 : Category) - -> Category ; - sumLObj: ({c1,c2} : Category) - -> Obj c1 - -> Obj (Sum c1 c2) ; - sumRObj: ({c1,c2} : Category) - -> Obj c2 - -> Obj (Sum c1 c2) ; - sumLAr : ({c1,c2} : Category) - -> ({x,y} : Obj c1) - -> Arrow x y - -> Arrow {Sum c1 c2} (sumLObj x) (sumLObj y) ; - sumRAr : ({c1,c2} : Category) - -> ({x,y} : Obj c2) - -> Arrow x y - -> Arrow {Sum c1 c2} (sumRObj x) (sumRObj y) ; - - def id (sumLObj x) = sumLAr (id x) ; - id (sumRObj x) = sumRAr (id x) ; - - comp (sumRAr f) (sumRAr g) = sumRAr (comp f g) ; - comp (sumLAr f) (sumLAr g) = sumLAr (comp f g) ; - -} diff --git a/examples/category-theory/CategoryTheory.gf b/examples/category-theory/CategoryTheory.gf deleted file mode 100644 index 6e3ed3e09..000000000 --- a/examples/category-theory/CategoryTheory.gf +++ /dev/null @@ -1,11 +0,0 @@ -abstract CategoryTheory - = Categories - , Morphisms - , InitialAndTerminal - , Functor - , NaturalTransform - , Equalizer - , Adjoints - , Monad -** { -} \ No newline at end of file diff --git a/examples/category-theory/Equalizer.gf b/examples/category-theory/Equalizer.gf deleted file mode 100644 index 4e12bd199..000000000 --- a/examples/category-theory/Equalizer.gf +++ /dev/null @@ -1,49 +0,0 @@ -abstract Equalizer = Morphisms ** { - -cat Equalizer ({c} : Category) ({x,y,z} : Obj c) (f,g : Arrow x y) (e : Arrow z x) ; - -data equalizer : ({c} : Category) - -> ({x,y,z} : Obj c) - -> (f,g : Arrow x y) - -> (e : Arrow z x) - -> EqAr (comp f e) (comp g e) - -> Equalizer f g e ; - -fun idEqualizer : ({c} : Category) - -> ({x,y} : Obj c) - -> (f : Arrow x y) - -> Equalizer f f (id x) ; -def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ; - -fun equalizer2mono : ({c} : Category) - -> ({x,y,z} : Obj c) - -> (f,g : Arrow x y) - -> (e : Arrow z x) - -> Equalizer f g e - -> Mono e ; --- def equalizer2mono = ... - -cat CoEqualizer ({c} : Category) ({x,y,z} : Obj c) (e : Arrow y z) (f,g : Arrow x y) ; - -data coequalizer : ({c} : Category) - -> ({x,y,z} : Obj c) - -> (e : Arrow y z) - -> (f,g : Arrow x y) - -> EqAr (comp e f) (comp e g) - -> CoEqualizer e f g ; - -fun idCoEqualizer : ({c} : Category) - -> ({x,y} : Obj c) - -> (f : Arrow x y) - -> CoEqualizer (id y) f f ; -def idCoEqualizer {c} {x} {y} f = coequalizer (id y) f f (eqCompR (eqRefl (id y)) f) ; - -fun coequalizer2epi : ({c} : Category) - -> ({x,y,z} : Obj c) - -> ({e} : Arrow y z) - -> ({f,g} : Arrow x y) - -> CoEqualizer e f g - -> Epi e ; --- def coequalizer2epi = ... - -} diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf deleted file mode 100644 index e70254839..000000000 --- a/examples/category-theory/Functor.gf +++ /dev/null @@ -1,53 +0,0 @@ -abstract Functor = Categories ** { - - ---------------------------------------------------------- - -- Functor - an arrow (a morphism) between two categories - -- - -- The functor is defined by two morphisms - one for the - -- objects and one for the arrows. We also require that - -- the morphisms preserve the categorial structure. - - cat Functor (c1, c2 : Category) ; - - data functor : ({c1, c2} : Category) - -> (f0 : Obj c1 -> Obj c2) - -> (f1 : ({x,y} : Obj c1) -> Arrow x y -> Arrow (f0 x) (f0 y)) - -> ((x : Obj c1) -> EqAr (f1 (id x)) (id (f0 x))) - -> (({x,y,z} : Obj c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f))) - -> Functor c1 c2 ; - - -- identity functor - fun idF : (c : Category) -> Functor c c ; - def idF c = functor (\x->x) (\f->f) (\x -> eqRefl (id x)) (\f,g -> eqRefl (comp g f)) ; - - -- composition of two functors - fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ; - def compF (functor f032 f132 eqid32 eqcmp32) (functor f013 f113 eqid13 eqcmp13) = - functor (\x -> f032 (f013 x)) - (\x -> f132 (f113 x)) - (\x -> eqTran (eqSym (mapEqAr f032 f132 (eqid13 x))) (eqid32 (f013 x))) - (\f,g -> eqTran (eqSym (mapEqAr f032 f132 (eqcmp13 f g))) (eqcmp32 (f113 f) (f113 g))) ; - - fun mapObj : ({c1, c2} : Category) - -> Functor c1 c2 - -> Obj c1 - -> Obj c2 ; - def mapObj (functor f0 f1 _ _) = f0 ; - - fun mapAr : ({c1, c2} : Category) - -> ({x,y} : Obj c1) - -> (f : Functor c1 c2) - -> Arrow x y - -> Arrow (mapObj f x) (mapObj f y) ; - def mapAr (functor f0 f1 _ _) = f1 ; - - fun mapEqAr : ({c1,c2} : Category) - -> ({x,y} : Obj c1) - -> ({f,g} : Arrow x y) - -> (f0 : Obj c1 -> Obj c2) - -> (f1 : Arrow x y -> Arrow (f0 x) (f0 y)) - -> EqAr f g - -> EqAr (f1 f) (f1 g) ; - def mapEqAr f0 f1 (eqRefl f) = eqRefl (f1 f) ; - -} 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 = .. ; - -} diff --git a/examples/category-theory/Monad.gf b/examples/category-theory/Monad.gf deleted file mode 100644 index 68612d312..000000000 --- a/examples/category-theory/Monad.gf +++ /dev/null @@ -1,30 +0,0 @@ -abstract Monad = Adjoints ** { - -cat Monad ({c} : Category) (m : Functor c c) ; - -data monad : ({c} : Category) - -> (m : Functor c c) - -> NT (compF m m) m - -> NT (idF c) m - -> Monad m ; - -fun adjoints2monad : ({c,d} : Category) - -> (f : Functor c d) - -> (g : Functor d c) - -> Adjoints f g - -> Monad (compF g f) ; --- def adjoints2monad = ... - -{- -fun kleisliCat : ({c} : Category) - -> ({m} : Functor c c) - -> Monad m - -> Category ; - -fun monad2adjoints : ({c} : Category) - -> ({m} : Functor c c) - -> Monad m - -> Adjoints {c} {kleisliCat m} f g --} - -} \ No newline at end of file diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf deleted file mode 100644 index 002a2656a..000000000 --- a/examples/category-theory/Morphisms.gf +++ /dev/null @@ -1,92 +0,0 @@ -abstract Morphisms = Categories ** { - -------------------------------------------------------- --- 1. Isomorphism - pair of arrows whose composition --- is the identity arrow - -cat Iso ({c} : Category) ({x,y} : Obj c) (Arrow x y) (Arrow y x) ; - -data iso : ({c} : Category) - -> ({x,y} : Obj c) - -> (f : Arrow x y) - -> (g : Arrow y x) - -> (EqAr (comp f g) (id y)) - -> (EqAr (comp g f) (id x)) - -> Iso f g ; - -fun isoOp : ({c} : Category) - -> ({x,y} : Obj c) - -> ({f} : Arrow x y) - -> ({g} : Arrow y x) - -> Iso f g - -> Iso (opAr g) (opAr f) ; -def isoOp (iso f g id_fg id_gf) = iso (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ; - --- every isomorphism is also monomorphism -fun iso2mono : ({c} : Category) - -> ({x,y} : Obj c) - -> ({f} : Arrow x y) - -> ({g} : Arrow y x) - -> (Iso f g -> Mono f) ; -def iso2mono (iso f g id_fg id_gf) = - mono f (\h,m,eq_fh_fm -> - eqSym (eqTran (eqIdR m) -- h = m - (eqTran (eqCompR id_gf m) -- id . m = h - (eqTran (eqAssoc g f m) -- (g . f) . m = h - (eqSym (eqTran (eqIdR h) -- g . (f . m) = h - (eqTran (eqCompR id_gf h) -- id . h = g . (f . m) - (eqTran (eqAssoc g f h) -- (g . f) . h = g . (f . m) - (eqCompL g eq_fh_fm))))))))) ; -- g . (f . h) = g . (f . m) - -- f . h = f . m - --- every isomorphism is also epimorphism -fun iso2epi : ({c} : Category) - -> ({x,y} : Obj c) - -> ({f} : Arrow x y) - -> ({g} : Arrow y x) - -> (Iso f g -> Epi f) ; - -def iso2epi (iso f g id_fg id_gf) = - epi f (\h,m,eq_hf_mf -> - eqSym (eqTran (eqIdL m) -- h = m - (eqTran (eqCompL m id_fg) -- m . id = h - (eqTran (eqSym (eqAssoc m f g)) -- m . (f . g) = h - (eqSym (eqTran (eqIdL h) -- (m . f) . g = h - (eqTran (eqCompL h id_fg) -- h . id = (m . f) . g - (eqTran (eqSym (eqAssoc h f g)) -- h . (f . g) = (m . f) . g - (eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g - -- h . f = m . f - - -------------------------------------------------------- --- 2. Monomorphism - an arrow f such that: --- --- f . h == f . m ==> h == m --- --- for every h and m. - -cat Mono ({c} : Category) ({x,y} : Obj c) (Arrow x y) ; - -data mono : ({c} : Category) - -> ({x,y} : Obj c) - -> (f : Arrow x y) - -> (({z} : Obj c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m) - -> Mono f ; - - -------------------------------------------------------- --- 3. Epimorphism - an arrow f such that: --- --- h . f == m . f ==> h == m --- --- for every h and m. - -cat Epi ({c} : Category) ({x,y} : Obj c) (Arrow x y) ; - -data epi : ({c} : Category) - -> ({x,y} : Obj c) - -> (f : Arrow x y) - -> (({z} : Obj c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m) - -> Epi f ; - -} diff --git a/examples/category-theory/NaturalTransform.gf b/examples/category-theory/NaturalTransform.gf deleted file mode 100644 index 60943737c..000000000 --- a/examples/category-theory/NaturalTransform.gf +++ /dev/null @@ -1,19 +0,0 @@ -abstract NaturalTransform = Functor ** { - - ---------------------------------------------------------- - -- Natural transformation - a pair of functors which - -- differ up to an arrow - - cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ; - - data nt : ({c1,c2} : Category) - -> (f,g : Functor c1 c2) - -> (n : (x : Obj c1) -> Arrow (mapObj f x) (mapObj g x)) - -> ( ({x,y} : Obj c1) - -> (ar : Arrow x y) - -> EqAr (comp (n y) (mapAr f ar)) - (comp (mapAr g ar) (n x)) - ) - -> NT f g ; - -} -- cgit v1.2.3