more category theory -> morphisms, initial and terminal objects

4 files changed, 102 insertions, 16 deletions

diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf
index 09c474290..71c6795df 100644
--- a/examples/category-theory/Categories.gf
+++ b/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)
diff --git a/examples/category-theory/CategoryTheory.gf b/examples/category-theory/CategoryTheory.gf
new file mode 100644
index 000000000..d896ceb35
--- /dev/null
+++ b/examples/category-theory/CategoryTheory.gf
@@ -0,0 +1,7 @@
+abstract CategoryTheory 

+  = Categories

+  , Morphisms

+  , InitialAndTerminal

+

+** {

+}
\ No newline at end of file
diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
new file mode 100644
index 000000000..7ac7b0864
--- /dev/null
+++ b/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 = .. ;

+

+}
\ No newline at end of file
diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf
new file mode 100644
index 000000000..426419cc0
--- /dev/null
+++ b/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 ;
+
+}
\ No newline at end of file