From 19851031e69d05e802eeabfe5db55e58583e1ba0 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Tue, 1 Jun 2010 06:03:19 +0000
Subject: cleanup the code for category theory

---
 examples/category-theory/InitialAndTerminal.gf | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

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

diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
index 856fc1788..ac665f856 100644
--- a/examples/category-theory/InitialAndTerminal.gf
+++ b/examples/category-theory/InitialAndTerminal.gf
@@ -11,13 +11,14 @@ fun initAr :  ({c} : Category)
            -> Initial x
            -> (y : El c)
            -> Arrow x y ;
-def initAr {c} {x} (initial {c} x f) y = f y ;
-
+-- def initAr {~c} {~x} (initial {c} x f) y = f y ;
+{-
 fun initials2iso :  ({c} : Category)
                  -> ({x,y} : El c)
                  -> (ix : Initial x)
                  -> (iy : Initial y)
                  -> Iso (initAr ix y) (initAr iy x) ;
+-}
 -- def initials2iso = .. ;
 
 
@@ -32,13 +33,14 @@ fun terminalAr :  ({c} : Category)
                -> ({y} : El c)
                -> Terminal y
                -> Arrow x y ;
-def terminalAr {c} x {y} (terminal {c} y f) = f x ;
-
+-- def terminalAr {c} x {~y} (terminal {~c} y f) = f x ;
+{-
 fun terminals2iso :  ({c} : Category)
                   -> ({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