From 9f45bb0df10f8367bff0851da5fea3129a0512c0 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Mon, 15 Mar 2010 10:43:20 +0000
Subject: refactor Morphisms.gf and InitialAndTerminal.gf

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

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

diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
index 3a033dcd5..856fc1788 100644
--- a/examples/category-theory/InitialAndTerminal.gf
+++ b/examples/category-theory/InitialAndTerminal.gf
@@ -1,35 +1,44 @@
 abstract InitialAndTerminal = Morphisms ** {
 
-cat  Initial  (c : Category) ;
+cat  Initial  ({c} : Category) (El c) ;
 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 {c} (initial {c} x f) = x ;
+              -> Initial x ;
+              
+fun initAr :  ({c} : Category)
+           -> ({x} : El c)
+           -> Initial x
+           -> (y : El c)
+           -> Arrow x y ;
+def initAr {c} {x} (initial {c} x f) y = f y ;
 
 fun initials2iso :  ({c} : Category)
-                 -> ({x,y} : Initial c)
-                 -> Iso (initEl x) (initEl y) ;
+                 -> ({x,y} : El c)
+                 -> (ix : Initial x)
+                 -> (iy : Initial y)
+                 -> Iso (initAr ix y) (initAr iy x) ;
 -- def initials2iso = .. ;
 
-cat  Terminal (c : Category) ;
+
+cat  Terminal ({c} : Category) (El c) ;
 data terminal : ({c} : Category)
               -> (y : El c)
               -> ((x : El c) -> Arrow x y)
-              -> Terminal c ;
+              -> Terminal y ;
 
-fun termEl : ({c} : Category)
-             -> Terminal c
-             -> El c ;
-def termEl {c} (terminal {c} x f) = x ;
+fun terminalAr :  ({c} : Category)
+               -> (x : El c)
+               -> ({y} : El c)
+               -> Terminal y
+               -> Arrow x y ;
+def terminalAr {c} x {y} (terminal {c} y f) = f x ;
 
 fun terminals2iso :  ({c} : Category)
-                  -> ({x,y} : Terminal c)
-                  -> Iso (termEl x) (termEl y) ;
+                  -> ({x,y} : El 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