some more definitions in category theory

2 files changed, 65 insertions, 31 deletions

diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf
index 71c6795df..e8f4b7955 100644
--- a/examples/category-theory/Categories.gf
+++ b/examples/category-theory/Categories.gf
@@ -15,29 +15,56 @@ abstract Categories = {
 
   fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ;
 
-      eq     : ({c} : Category)
+  data eqRefl : ({c} : Category)
+              -> ({x,y} : El c)
+              -> (a : Arrow x y)
+              -> EqAr a a ;
+  fun  eqSym  : ({c} : Category)
+              -> ({x,y} : El c)
+              -> ({a,b} : Arrow x y)
+              -> EqAr a b
+              -> EqAr b a ;
+  def  eqSym {c} {x} {y} {a} {a} (eqRefl {c} {x} {y} a) = eqRefl a ;
+              
+  fun eqTran :  ({c} : Category)
              -> ({x,y} : El c)
-             -> (a : Arrow x y)
-             -> EqAr a a ;
-      eqRefl : ({c} : Category)
-             -> ({x,y} : El c)
-             -> ({a,b} : Arrow x y)
-             -> EqAr a b
-             -> EqAr b a ;
-      eqIdL  : ({c} : Category)
+             -> ({f,g,h} : Arrow x y)
+             -> EqAr f g
+             -> EqAr f h
+             -> EqAr g h ;
+  def eqTran {c} {x} {y} {a} {a} {b} (eqRefl {c} {x} {y} a) eq = eq ;
+
+  fun eqCompL :  ({c} : Category)
+              -> ({x,y,z} : El c)
+              -> ({g,h} : Arrow x z)
+              -> (f : Arrow z y)
+              -> EqAr g h
+              -> EqAr (comp f g) (comp f h) ;
+  def eqCompL {c} {x} {y} {z} {g} {g} f (eqRefl {c} {x} {z} g) = eqRefl (comp f g) ;
+
+  fun eqCompR :  ({c} : Category)
+              -> ({x,y,z} : El c)
+              -> ({g,h} : Arrow z y)
+              -> EqAr g h
+              -> (f : Arrow x z)
+              -> EqAr (comp g f) (comp h f) ;
+  def eqCompR {c} {x} {y} {z} {g} {g} (eqRefl {c} {z} {y} g) f = eqRefl (comp g f) ;
+
+  fun eqIdL  : ({c} : Category)
              -> ({x,y} : El c)
              -> (a : Arrow x y)
-             -> EqAr a (comp a (id x)) ;
-      eqIdR  : ({c} : Category)
+             -> EqAr (comp a (id x)) a ;
+      eqIdR  :  ({c} : Category)
              -> ({x,y} : El c)
              -> (a : Arrow x y)
-             -> EqAr a (comp (id y) a) ;
-      eqComp :  ({c} : Category) 
-             -> ({w,x,y,z} : El c)
-             -> (f : Arrow w y)
-             -> (g : Arrow z w)
-             -> (h : Arrow x z)
-             -> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
+             -> EqAr (comp (id y) a) a ;
+
+  fun eqAssoc :  ({c} : Category)
+              -> ({w,x,y,z} : El c)
+              -> (f : Arrow w y)
+              -> (g : Arrow z w)
+              -> (h : Arrow x z)
+              -> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
 
   data Op   :  (c : Category)
             -> Category ;
@@ -48,6 +75,8 @@ abstract Categories = {
             -> ({x,y} : El c)
             -> (a : Arrow x y)
             -> Arrow {Op c} (opEl y) (opEl x) ;
+  def  id {Op c} (opEl {c} x) = opAr (id x) ;
+  def  comp {Op c} {opEl {c} x} {opEl {c} y} {opEl {c} z} (opAr {c} {y} {z} f) (opAr {c} {z} {x} g) = opAr (comp g f) ;
 
   data Slash     :  (c : Category)
                  -> (x : El c)
@@ -62,8 +91,8 @@ abstract Categories = {
                  -> ({az} : Arrow z x)
                  -> Arrow y z
                  -> Arrow (slashEl x ay) (slashEl x az) ;
-
-  def  id (slashEl x {y} a) = slashAr x (id y) ;
+  def  id {Slash c x} (slashEl {c} x {y} a) = slashAr x {y} {y} {a} {a} (id y) ;
+  def  comp {Slash c t} {slashEl {c} t {x} ax} {slashEl {c} t {y} ay} {slashEl {c} t {z} az} (slashAr {c} t {z} {y} {az} {ay} azy) (slashAr {c} t {x} {z} {ax} {az} axz) = slashAr t {x} {y} {ax} {ay} (comp azy axz) ;
 
   data CoSlash   :  (c : Category)
                  -> (x : El c)
@@ -75,10 +104,11 @@ abstract Categories = {
        coslashAr :  ({c} : Category)
                  -> (x,{y,z} : El c)
                  -> ({ay} : Arrow x y)
-                 -> ({az} : Arrow x y)
+                 -> ({az} : Arrow x z)
                  -> Arrow z y
                  -> Arrow (coslashEl x ay) (coslashEl x az) ;
-  def  id (coslashEl x {y} a) = coslashAr x (id y) ;
+  def  id {CoSlash c x} (coslashEl {c} x {y} a) = coslashAr x (id y) ;
+  def  comp {CoSlash c t} {coslashEl {c} t {x} ax} {coslashEl {c} t {y} ay} {coslashEl {c} t {z} az} (coslashAr {c} t {z} {y} {az} {ay} ayz) (coslashAr {c} t {x} {z} {ax} {az} azx) = coslashAr t {x} {y} {ax} {ay} (comp azx ayz) ;
 
   data Prod   :  (c1,c2 : Category)
               -> Category ;
@@ -92,13 +122,14 @@ abstract Categories = {
               -> Arrow x1 y1
               -> Arrow x2 y2
               -> Arrow (prodEl x1 x2) (prodEl y1 y2) ;
-  def  id (prodEl x1 x2) = prodAr (id x1) (id x2) ;
+  def id {Prod c1 c2} (prodEl {c1} {c2} x1 x2) = prodAr (id x1) (id x2) ;
+  def comp {Prod c1 c2} {prodEl {c1} {c2} x1 x2} {prodEl {c1} {c2} y1 y2} {prodEl {c1} {c2} z1 z2} (prodAr {c1} {c2} {z1} {y1} {z2} {y2} f1 f2) (prodAr {c1} {c2} {x1} {z1} {x2} {z2} g1 g2) = prodAr {c1} {c2} {x1} {y1} {x2} {y2} (comp f1 g1) (comp f2 g2) ;
   
   fun fst : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c1 ;
-  def fst (prodEl x1 _) = x1 ;
+  def fst {c1} {c2} (prodEl {c1} {c2} x1 _) = x1 ;
 
   fun snd : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c2 ;
-  def snd (prodEl _ x2) = x2 ;
+  def snd {c1} {c2} (prodEl {c1} {c2} _ x2) = x2 ;
 
   data Sum    :  (c1,c2 : Category)
               -> Category ;
@@ -111,12 +142,15 @@ abstract Categories = {
        sumLAr :  ({c1,c2} : Category)
               -> ({x,y} : El c1)
               -> Arrow x y
-              -> Arrow (sumLEl x) (sumLEl y) ;
+              -> Arrow {Sum c1 c2} (sumLEl x) (sumLEl y) ;
        sumRAr :  ({c1,c2} : Category)
               -> ({x,y} : El c2)
               -> Arrow x y
-              -> Arrow (sumREl x) (sumREl y) ;
-  def  id (sumLEl x) = sumLAr (id x) ;
-       id (sumREl x) = sumRAr (id x) ;
+              -> Arrow {Sum c1 c2} (sumREl x) (sumREl y) ;
+  def  id {Sum c1 c2} (sumLEl {c1} {c2} x) = sumLAr (id x) ;
+       id {Sum c1 c2} (sumREl {c1} {c2} x) = sumRAr (id x) ;
+
+       comp {Sum c1 c2} {sumREl {c1} {c2} x} {sumREl {c1} {c2} y} {sumREl {c1} {c2} z} (sumRAr {c1} {c2} {z} {y} f) (sumRAr {c1} {c2} {x} {z} g) = sumRAr (comp f g) ;
+       comp {Sum c1 c2} {sumLEl {c1} {c2} x} {sumLEl {c1} {c2} y} {sumLEl {c1} {c2} z} (sumLAr {c1} {c2} {z} {y} f) (sumLAr {c1} {c2} {x} {z} g) = sumLAr (comp f g) ;
 
 }
\ No newline at end of file
diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
index 7ac7b0864..3a033dcd5 100644
--- a/examples/category-theory/InitialAndTerminal.gf
+++ b/examples/category-theory/InitialAndTerminal.gf
@@ -9,7 +9,7 @@ data initial  : ({c} : Category)
 fun initEl : ({c} : Category)

               -> Initial c

               -> El c ;

-def initEl (initial x f) = x ;

+def initEl {c} (initial {c} x f) = x ;

 

 fun initials2iso :  ({c} : Category)

                  -> ({x,y} : Initial c)

@@ -25,7 +25,7 @@ data terminal : ({c} : Category)
 fun termEl : ({c} : Category)

              -> Terminal c

              -> El c ;

-def termEl (terminal x f) = x ;

+def termEl {c} (terminal {c} x f) = x ;

 

 fun terminals2iso :  ({c} : Category)

                   -> ({x,y} : Terminal c)