El -> Obj in category theory

1 files changed, 13 insertions, 13 deletions

diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
index ac665f856..b8a9f00c9 100644
--- a/examples/category-theory/InitialAndTerminal.gf
+++ b/examples/category-theory/InitialAndTerminal.gf
@@ -1,20 +1,20 @@
 abstract InitialAndTerminal = Morphisms ** {

 

-cat  Initial  ({c} : Category) (El c) ;

+cat  Initial  ({c} : Category) (Obj c) ;

 data initial  : ({c} : Category)

-              -> (x : El c)

-              -> ((y : El c) -> Arrow x y)

+              -> (x : Obj c)

+              -> ((y : Obj c) -> Arrow x y)

               -> Initial x ;

               

 fun initAr :  ({c} : Category)

-           -> ({x} : El c)

+           -> ({x} : Obj c)

            -> Initial x

-           -> (y : El c)

+           -> (y : Obj c)

            -> Arrow x y ;

 -- def initAr {~c} {~x} (initial {c} x f) y = f y ;

 {-

 fun initials2iso :  ({c} : Category)

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

+                 -> ({x,y} : Obj c)

                  -> (ix : Initial x)

                  -> (iy : Initial y)

                  -> Iso (initAr ix y) (initAr iy x) ;

@@ -22,25 +22,25 @@ fun initials2iso :  ({c} : Category)
 -- def initials2iso = .. ;

 

 

-cat  Terminal ({c} : Category) (El c) ;

+cat  Terminal ({c} : Category) (Obj c) ;

 data terminal : ({c} : Category)

-              -> (y : El c)

-              -> ((x : El c) -> Arrow x y)

+              -> (y : Obj c)

+              -> ((x : Obj c) -> Arrow x y)

               -> Terminal y ;

 

 fun terminalAr :  ({c} : Category)

-               -> (x : El c)

-               -> ({y} : El c)

+               -> (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} : El c)

+                  -> ({x,y} : Obj c)

                   -> (tx : Terminal x)

                   -> (ty : Terminal y)

                   -> Iso (terminalAr x ty) (terminalAr y tx) ;

                   -}

 -- def terminals2iso = .. ;

 

-}
\ No newline at end of file
+}