some more definitions in category theory

1 files changed, 2 insertions, 2 deletions

diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
index 7ac7b0864..3a033dcd5 100644
--- a/examples/category-theory/InitialAndTerminal.gf
+++ b/examples/category-theory/InitialAndTerminal.gf
@@ -9,7 +9,7 @@ data initial  : ({c} : Category)
 fun initEl : ({c} : Category)

               -> Initial c

               -> El c ;

-def initEl (initial x f) = x ;

+def initEl {c} (initial {c} x f) = x ;

 

 fun initials2iso :  ({c} : Category)

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

@@ -25,7 +25,7 @@ data terminal : ({c} : Category)
 fun termEl : ({c} : Category)

              -> Terminal c

              -> El c ;

-def termEl (terminal x f) = x ;

+def termEl {c} (terminal {c} x f) = x ;

 

 fun terminals2iso :  ({c} : Category)

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