El -> Obj in category theory

6 files changed, 106 insertions, 106 deletions

diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf
index 91a30c61b..00fcdad7e 100644
--- a/examples/category-theory/Categories.gf
+++ b/examples/category-theory/Categories.gf
@@ -1,33 +1,33 @@
 abstract Categories = {
 
   cat Category ;
-      El Category ;
-      Arrow ({c} : Category) (El c) (El c) ;
-      EqAr ({c} : Category) ({x,y} : El c) (f,g : Arrow x y) ;
+      Obj Category ;
+      Arrow ({c} : Category) (Obj c) (Obj c) ;
+      EqAr ({c} : Category) ({x,y} : Obj c) (f,g : Arrow x y) ;
 
-  fun dom : ({c} : Category) -> ({x,y} : El c) -> Arrow x y -> El c ;
+  fun dom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
   def dom   {_} {x} {y} _ = x ;
 
-  fun codom : ({c} : Category) -> ({x,y} : El c) -> Arrow x y -> El c ;
+  fun codom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
   def codom {_} {x} {y} _ = y ;
 
-  fun id   : ({c} : Category) -> (x : El c) -> Arrow x x ;
+  fun id   : ({c} : Category) -> (x : Obj c) -> Arrow x x ;
 
-  fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ;
+  fun comp : ({c} : Category) -> ({x,y,z} : Obj c) -> Arrow z y -> Arrow x z -> Arrow x y ;
 
   data eqRefl :  ({c} : Category)
-              -> ({x,y} : El c)
+              -> ({x,y} : Obj c)
               -> (a : Arrow x y)
               -> EqAr a a ;
   fun  eqSym  : ({c} : Category)
-              -> ({x,y} : El c)
+              -> ({x,y} : Obj c)
               -> ({a,b} : Arrow x y)
               -> EqAr a b
               -> EqAr b a ;
   def  eqSym (eqRefl a) = eqRefl a ;
 
   fun eqTran :  ({c} : Category)
-             -> ({x,y} : El c)
+             -> ({x,y} : Obj c)
              -> ({f,g,h} : Arrow x y)
              -> EqAr f g
              -> EqAr f h
@@ -35,7 +35,7 @@ abstract Categories = {
   def eqTran (eqRefl a) eq = eq ;
 
   fun eqCompL :  ({c} : Category)
-              -> ({x,y,z} : El c)
+              -> ({x,y,z} : Obj c)
               -> ({g,h} : Arrow x z)
               -> (f : Arrow z y)
               -> EqAr g h
@@ -43,7 +43,7 @@ abstract Categories = {
   def eqCompL f (eqRefl g) = eqRefl (comp f g) ;
 
   fun eqCompR :  ({c} : Category)
-              -> ({x,y,z} : El c)
+              -> ({x,y,z} : Obj c)
               -> ({g,h} : Arrow z y)
               -> EqAr g h
               -> (f : Arrow x z)
@@ -51,16 +51,16 @@ abstract Categories = {
   def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
 
   fun eqIdL  : ({c} : Category)
-             -> ({x,y} : El c)
+             -> ({x,y} : Obj c)
              -> (a : Arrow x y)
              -> EqAr (comp a (id x)) a ;
       eqIdR  :  ({c} : Category)
-             -> ({x,y} : El c)
+             -> ({x,y} : Obj c)
              -> (a : Arrow x y)
              -> EqAr (comp (id y) a) a ;
 
   fun eqAssoc :  ({c} : Category)
-              -> ({w,x,y,z} : El c)
+              -> ({w,x,y,z} : Obj c)
               -> (f : Arrow w y)
               -> (g : Arrow z w)
               -> (h : Arrow x z)
@@ -68,18 +68,18 @@ abstract Categories = {
 
   data Op   :  (c : Category)
             -> Category ;
-       opEl :  ({c} : Category)
-            -> (x : El c)
-            -> El (Op c) ;
+       opObj:  ({c} : Category)
+            -> (x : Obj c)
+            -> Obj (Op c) ;
        opAr :  ({c} : Category)
-            -> ({x,y} : El c)
+            -> ({x,y} : Obj c)
             -> (a : Arrow x y)
-            -> Arrow {Op c} (opEl y) (opEl x) ;
-  def  id (opEl x) = opAr (id x) ;
+            -> Arrow {Op c} (opObj y) (opObj x) ;
+  def  id (opObj x) = opAr (id x) ;
   def  comp (opAr f) (opAr g) = opAr (comp g f) ;
 
   fun eqOp :  ({c} : Category)
-           -> ({x,y} : El c)
+           -> ({x,y} : Obj c)
            -> ({f} : Arrow x y)
            -> ({g} : Arrow x y)
            -> EqAr f g
@@ -87,77 +87,77 @@ abstract Categories = {
   def eqOp (eqRefl f) = eqRefl (opAr f) ;
 
   data Slash     :  (c : Category)
-                 -> (x : El c)
+                 -> (x : Obj c)
                  -> Category ;
-       slashEl   :  ({c} : Category)
-                 -> (x,{y} : El c)
+       slashObj  :  ({c} : Category)
+                 -> (x,{y} : Obj c)
                  -> Arrow y x
-                 -> El (Slash c x) ;
+                 -> Obj (Slash c x) ;
        slashAr   :  ({c} : Category)
-                 -> (x,{y,z} : El c)
+                 -> (x,{y,z} : Obj c)
                  -> ({ay} : Arrow y x)
                  -> ({az} : Arrow z x)
                  -> Arrow y z
-                 -> Arrow (slashEl x ay) (slashEl x az) ;
-  def  id (slashEl x {y} a) = slashAr x (id y) ;
+                 -> Arrow (slashObj x ay) (slashObj x az) ;
+  def  id (slashObj x {y} a) = slashAr x (id y) ;
   def  comp (slashAr t azy) (slashAr ~t axz) = slashAr t (comp azy axz) ;
 
   data CoSlash   :  (c : Category)
-                 -> (x : El c)
+                 -> (x : Obj c)
                  -> Category ;
-       coslashEl :  ({c} : Category)
-                 -> (x,{y} : El c)
+       coslashObj:  ({c} : Category)
+                 -> (x,{y} : Obj c)
                  -> Arrow x y
-                 -> El (CoSlash c x) ;
+                 -> Obj (CoSlash c x) ;
        coslashAr :  ({c} : Category)
-                 -> (x,{y,z} : El c)
+                 -> (x,{y,z} : Obj c)
                  -> ({ay} : 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) ;
+                 -> Arrow (coslashObj x ay) (coslashObj x az) ;
+  def  id (coslashObj x {y} a) = coslashAr x (id y) ;
   def  comp (coslashAr t ayz) (coslashAr ~t azx) = coslashAr t (comp azx ayz) ;
 
   data Prod   :  (c1,c2 : Category)
               -> Category ;
-       prodEl :  ({c1,c2} : Category)
-              -> El c1
-              -> El c2
-              -> El (Prod c1 c2) ;
+       prodObj:  ({c1,c2} : Category)
+              -> Obj c1
+              -> Obj c2
+              -> Obj (Prod c1 c2) ;
        prodAr :  ({c1,c2} : Category)
-              -> ({x1,y1} : El c1)
-              -> ({x2,y2} : El c2)
+              -> ({x1,y1} : Obj c1)
+              -> ({x2,y2} : Obj c2)
               -> Arrow x1 y1
               -> Arrow x2 y2
-              -> Arrow (prodEl x1 x2) (prodEl y1 y2) ;
-  def id (prodEl x1 x2) = prodAr (id x1) (id x2) ;
+              -> Arrow (prodObj x1 x2) (prodObj y1 y2) ;
+  def id (prodObj x1 x2) = prodAr (id x1) (id x2) ;
   def comp (prodAr f1 f2) (prodAr g1 g2) = prodAr (comp f1 g1) (comp f2 g2) ;
 
-  fun fst : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c1 ;
-  def fst (prodEl x1 _) = x1 ;
+  fun fst : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c1 ;
+  def fst (prodObj x1 _) = x1 ;
 
-  fun snd : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c2 ;
-  def snd (prodEl _ x2) = x2 ;
+  fun snd : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c2 ;
+  def snd (prodObj _ x2) = x2 ;
   
   data Sum    :  (c1,c2 : Category)
               -> Category ;
-       sumLEl :  ({c1,c2} : Category)
-              -> El c1
-              -> El (Sum c1 c2) ;
-       sumREl :  ({c1,c2} : Category)
-              -> El c2
-              -> El (Sum c1 c2) ;
+       sumLObj:  ({c1,c2} : Category)
+              -> Obj c1
+              -> Obj (Sum c1 c2) ;
+       sumRObj:  ({c1,c2} : Category)
+              -> Obj c2
+              -> Obj (Sum c1 c2) ;
        sumLAr :  ({c1,c2} : Category)
-              -> ({x,y} : El c1)
+              -> ({x,y} : Obj c1)
               -> Arrow x y
-              -> Arrow {Sum c1 c2} (sumLEl x) (sumLEl y) ;
+              -> Arrow {Sum c1 c2} (sumLObj x) (sumLObj y) ;
        sumRAr :  ({c1,c2} : Category)
-              -> ({x,y} : El c2)
+              -> ({x,y} : Obj c2)
               -> Arrow x y
-              -> Arrow {Sum c1 c2} (sumREl x) (sumREl y) ;
+              -> Arrow {Sum c1 c2} (sumRObj x) (sumRObj y) ;
 
-  def  id (sumLEl x) = sumLAr (id x) ;
-       id (sumREl x) = sumRAr (id x) ;
+  def  id (sumLObj x) = sumLAr (id x) ;
+       id (sumRObj x) = sumRAr (id x) ;
 
        comp (sumRAr f) (sumRAr g) = sumRAr (comp f g) ;
        comp (sumLAr f) (sumLAr g) = sumLAr (comp f g) ;
diff --git a/examples/category-theory/Equalizer.gf b/examples/category-theory/Equalizer.gf
index 051a19200..4e12bd199 100644
--- a/examples/category-theory/Equalizer.gf
+++ b/examples/category-theory/Equalizer.gf
@@ -1,49 +1,49 @@
 abstract Equalizer = Morphisms ** {
 
-cat Equalizer ({c} : Category) ({x,y,z} : El c) (f,g : Arrow x y) (e : Arrow z x) ;
+cat Equalizer ({c} : Category) ({x,y,z} : Obj c) (f,g : Arrow x y) (e : Arrow z x) ;
 
 data equalizer :  ({c} : Category)
-               -> ({x,y,z} : El c)
+               -> ({x,y,z} : Obj c)
                -> (f,g : Arrow x y)
                -> (e : Arrow z x)
                -> EqAr (comp f e) (comp g e)
                -> Equalizer f g e ;
 
 fun idEqualizer : ({c} : Category)
-               -> ({x,y} : El c)
+               -> ({x,y} : Obj c)
                -> (f : Arrow x y)
                -> Equalizer f f (id x) ;
 def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ;
 
 fun equalizer2mono :  ({c} : Category)
-                   -> ({x,y,z} : El c)
+                   -> ({x,y,z} : Obj c)
                    -> (f,g : Arrow x y)
                    -> (e : Arrow z x)
                    -> Equalizer f g e
                    -> Mono e ;
 -- def equalizer2mono = ...
 
-cat CoEqualizer ({c} : Category) ({x,y,z} : El c) (e : Arrow y z) (f,g : Arrow x y) ;
+cat CoEqualizer ({c} : Category) ({x,y,z} : Obj c) (e : Arrow y z) (f,g : Arrow x y) ;
 
 data coequalizer :  ({c} : Category)
-                 -> ({x,y,z} : El c)
+                 -> ({x,y,z} : Obj c)
                  -> (e : Arrow y z)
                  -> (f,g : Arrow x y)
                  -> EqAr (comp e f) (comp e g)
                  -> CoEqualizer e f g ;
 
 fun idCoEqualizer : ({c} : Category)
-                 -> ({x,y} : El c)
+                 -> ({x,y} : Obj c)
                  -> (f : Arrow x y)
                  -> CoEqualizer (id y) f f ;
 def idCoEqualizer {c} {x} {y} f = coequalizer (id y) f f (eqCompR (eqRefl (id y)) f) ;
 
 fun coequalizer2epi :  ({c} : Category)
-                    -> ({x,y,z} : El c)
+                    -> ({x,y,z} : Obj c)
                     -> ({e} : Arrow y z)
                     -> ({f,g} : Arrow x y)
                     -> CoEqualizer e f g
                     -> Epi e ;
 -- def coequalizer2epi = ...
 
-}
\ No newline at end of file
+}
diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf
index 2c638eab9..45f519edf 100644
--- a/examples/category-theory/Functor.gf
+++ b/examples/category-theory/Functor.gf
@@ -3,10 +3,10 @@ abstract Functor = Categories ** {
 cat Functor (c1, c2 : Category) ;

 

 data functor :  ({c1, c2} : Category) 

-             -> (f0 : El c1 -> El c2)

-             -> (f1 : ({x,y} : El c1) -> Arrow x y -> Arrow (f0 x) (f0 y))

-             -> ((x : El c1) -> EqAr (f1 (id x)) (id (f0 x)))

-             -> (({x,y,z} : El c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f)))

+             -> (f0 : Obj c1 -> Obj c2)

+             -> (f1 : ({x,y} : Obj c1) -> Arrow x y -> Arrow (f0 x) (f0 y))

+             -> ((x : Obj c1) -> EqAr (f1 (id x)) (id (f0 x)))

+             -> (({x,y,z} : Obj c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f)))

              -> Functor c1 c2 ;

 

 fun idF : (c : Category) -> Functor c c ;

@@ -16,21 +16,21 @@ fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor
 def compF (functor f032 f132 eqid32 eqcmp32) (functor f013 f113 eqid13 eqcmp13) =

          functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr f132 eqid13) ? ;

 

-fun mapEl :  ({c1, c2} : Category)

+fun mapObj :  ({c1, c2} : Category)

           -> Functor c1 c2

-          -> El c1

-          -> El c2 ;

-def mapEl (functor f0 f1 _ _) = f0 ;

+          -> Obj c1

+          -> Obj c2 ;

+def mapObj (functor f0 f1 _ _) = f0 ;

 

 fun mapAr :  ({c1, c2} : Category)

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

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

           -> (f : Functor c1 c2)

           -> Arrow x y

-          -> Arrow (mapEl f x) (mapEl f y) ;

+          -> Arrow (mapObj f x) (mapObj f y) ;

 def mapAr (functor f0 f1 _ _) = f1 ;

 

 fun mapEqAr :  ({c} : Category)

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

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

             -> ({f,g} : Arrow x y)

             -> (func : Arrow x y -> Arrow x y)

             -> EqAr f g

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
+}

diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf
index df40f5abe..e86059115 100644
--- a/examples/category-theory/Morphisms.gf
+++ b/examples/category-theory/Morphisms.gf
@@ -1,9 +1,9 @@
 abstract Morphisms = Categories ** {
 
-cat Iso ({c} : Category) ({x,y} : El c) (Arrow x y) (Arrow y x) ;
+cat Iso ({c} : Category) ({x,y} : Obj c) (Arrow x y) (Arrow y x) ;
 
 data iso :  ({c} : Category)
-         -> ({x,y} : El c)
+         -> ({x,y} : Obj c)
          -> (f : Arrow x y)
          -> (g : Arrow y x)
          -> (EqAr (comp f g) (id y))
@@ -11,7 +11,7 @@ data iso :  ({c} : Category)
          -> Iso f g ;
 
 fun isoOp : ({c} : Category)
-         -> ({x,y} : El c)
+         -> ({x,y} : Obj c)
          -> ({f} : Arrow x y)
          -> ({g} : Arrow y x)
          -> Iso f g
@@ -19,7 +19,7 @@ fun isoOp : ({c} : Category)
 def isoOp (iso f g id_fg id_gf) = iso (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ;
 
 fun iso2mono :  ({c} : Category)
-             -> ({x,y} : El c)
+             -> ({x,y} : Obj c)
              -> ({f} : Arrow x y)
              -> ({g} : Arrow y x)
              -> (Iso f g -> Mono f) ;
@@ -35,7 +35,7 @@ def iso2mono (iso f g id_fg id_gf) =
                                                                                                                    --      f . h  = f . m
 
 fun iso2epi  :  ({c} : Category)
-             -> ({x,y} : El c)
+             -> ({x,y} : Obj c)
              -> ({f} : Arrow x y)
              -> ({g} : Arrow y x)
              -> (Iso f g -> Epi f) ;
@@ -51,20 +51,20 @@ def iso2epi (iso fff g id_fg id_gf) =
                                                                                    (eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g
                                                                                                                   --  h . f      =  m . f
 
-cat Mono ({c} : Category) ({x,y} : El c) (Arrow x y) ;
+cat Mono ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
 
 data mono :  ({c} : Category)
-          -> ({x,y} : El c)
+          -> ({x,y} : Obj c)
           -> (f : Arrow x y)
-          -> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
+          -> (({z} : Obj c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
           -> Mono f ;
 
-cat Epi ({c} : Category) ({x,y} : El c) (Arrow x y) ;
+cat Epi ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
 
 data epi  :  ({c} : Category)
-          -> ({x,y} : El c)
+          -> ({x,y} : Obj c)
           -> (f : Arrow x y)
-          -> (({z} : El c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
+          -> (({z} : Obj c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
           -> Epi f ;
 
 }
diff --git a/examples/category-theory/NaturalTransform.gf b/examples/category-theory/NaturalTransform.gf
index 01a7a65ef..6a3462985 100644
--- a/examples/category-theory/NaturalTransform.gf
+++ b/examples/category-theory/NaturalTransform.gf
@@ -4,7 +4,7 @@ cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
 
 data nt :  ({c1,c2} : Category)
         -> (f,g : Functor c1 c2)
-        -> ((x : El c1) -> Arrow (mapEl f x) (mapEl g x))
+        -> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
         -> NT f g ;
 
-}
\ No newline at end of file
+}