cleanup the code for category theory

1 files changed, 6 insertions, 4 deletions

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