From 5e0d04d0f59e4ace8df23befcbe8263447611e63 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Tue, 1 Jun 2010 06:12:30 +0000
Subject: El -> Obj in category theory

---
 examples/category-theory/InitialAndTerminal.gf | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'examples/category-theory/InitialAndTerminal.gf')

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
+}
-- 
cgit v1.2.3