more category theory -> morphisms, initial and terminal objects

examples/category-theory/Categories.gf

@@ -13,8 +13,8 @@ abstract Categories = {
 
   fun id   : ({c} : Category) -> (x : El c) -> Arrow x x ;
 
-  fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow x y -> Arrow y z -> Arrow x z ;
-      
+  fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ;
+
       eq     : ({c} : Category)
              -> ({x,y} : El c)
              -> (a : Arrow x y)
@@ -27,27 +27,27 @@ abstract Categories = {
       eqIdL  : ({c} : Category)
              -> ({x,y} : El c)
              -> (a : Arrow x y)
-             -> EqAr a (comp a (id y)) ;
+             -> EqAr a (comp a (id x)) ;
       eqIdR  : ({c} : Category)
              -> ({x,y} : El c)
              -> (a : Arrow x y)
-             -> EqAr a (comp (id x) a) ;
+             -> EqAr a (comp (id y) a) ;
       eqComp :  ({c} : Category) 
              -> ({w,x,y,z} : El c)
-             -> (f : Arrow w x)
-             -> (g : Arrow x y)
-             -> (h : Arrow y z)
+             -> (f : Arrow w y)
+             -> (g : Arrow z w)
+             -> (h : Arrow x z)
              -> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
 
-  fun Op   :  (c : Category)
-           -> Category ;
-      opEl :  ({c} : Category)
-           -> (x : El c)
-           -> El (Op c) ;
-      opAr :  ({c} : Category)
-           -> ({x,y} : El c)
-           -> (a : Arrow x y)
-           -> Arrow {Op c} (opEl y) (opEl x) ;
+  data Op   :  (c : Category)
+            -> Category ;
+       opEl :  ({c} : Category)
+            -> (x : El c)
+            -> El (Op c) ;
+       opAr :  ({c} : Category)
+            -> ({x,y} : El c)
+            -> (a : Arrow x y)
+            -> Arrow {Op c} (opEl y) (opEl x) ;
 
   data Slash     :  (c : Category)
                  -> (x : El c)

examples/category-theory/CategoryTheory.gf

@@ -0,0 +1,7 @@
+abstract CategoryTheory 
+  = Categories
+  , Morphisms
+  , InitialAndTerminal
+
+** {
+}

examples/category-theory/InitialAndTerminal.gf

@@ -0,0 +1,35 @@
+abstract InitialAndTerminal = Morphisms ** {
+
+cat  Initial  (c : Category) ;
+data initial  : ({c} : Category)
+              -> (x : El c)
+              -> ((y : El c) -> Arrow x y)
+              -> Initial c ;
+
+fun initEl : ({c} : Category)
+              -> Initial c
+              -> El c ;
+def initEl (initial x f) = x ;
+
+fun initials2iso :  ({c} : Category)
+                 -> ({x,y} : Initial c)
+                 -> Iso (initEl x) (initEl y) ;
+-- def initials2iso = .. ;
+
+cat  Terminal (c : Category) ;
+data terminal : ({c} : Category)
+              -> (y : El c)
+              -> ((x : El c) -> Arrow x y)
+              -> Terminal c ;
+
+fun termEl : ({c} : Category)
+             -> Terminal c
+             -> El c ;
+def termEl (terminal x f) = x ;
+
+fun terminals2iso :  ({c} : Category)
+                  -> ({x,y} : Terminal c)
+                  -> Iso (termEl x) (termEl y) ;
+-- def terminals2iso = .. ;
+
+}

examples/category-theory/Morphisms.gf

@@ -0,0 +1,44 @@
+abstract Morphisms = Categories ** {
+
+cat Iso ({c} : Category) (x,y : El c) ;
+
+data iso :  ({c} : Category)
+         -> ({x,y} : El c)
+         -> (f : Arrow x y)
+         -> (g : Arrow y x)
+         -> (EqAr (comp f g) (id y))
+         -> (EqAr (comp g f) (id x))
+         -> Iso x y ;
+
+fun iso2mono :  ({c} : Category)
+             -> ({x,y} : El c)
+             -> (Iso x y -> Mono x y) ;
+-- def iso2mono (iso f g eq_fg eq_gf) = (mono f (\h m eq_fh_fm -> ...))
+
+-- eqIdR (eqTran eq_gf (eqComp g f h)) : EqAr (comp g (comp f h)) h
+-- comp g (comp f m)
+
+fun iso2epi  :  ({c} : Category)
+             -> ({x,y} : El c)
+             -> (Iso x y -> Epi x y) ;
+-- def iso2epi (iso f g eq_fg eq_gf) = (epi f (\h m eq_hf_mf -> ...))
+
+
+cat Mono ({c} : Category) (x,y : El c) ;
+
+data mono :  ({c} : Category)
+          -> ({x,y} : El c)
+          -> (f : Arrow x y)
+          -> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
+          -> Mono x y ;
+
+
+cat Epi ({c} : Category) (x,y : El c) ;
+
+data epi  :  ({c} : Category)
+          -> ({x,y} : El c)
+          -> (f : Arrow x y)
+          -> (({z} : El c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
+          -> Epi x y ;
+
+}