diff options
| author | krasimir <krasimir@chalmers.se> | 2010-03-15 10:43:20 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-03-15 10:43:20 +0000 |
| commit | 9f45bb0df10f8367bff0851da5fea3129a0512c0 (patch) | |
| tree | be8279a1706be8c917f4cff16b69f389e8cb6312 /examples/category-theory/InitialAndTerminal.gf | |
| parent | d7c68cdf27a5e4a6b9dc402ae5d49fdf85321715 (diff) | |
refactor Morphisms.gf and InitialAndTerminal.gf
Diffstat (limited to 'examples/category-theory/InitialAndTerminal.gf')
| -rw-r--r-- | examples/category-theory/InitialAndTerminal.gf | 43 |
1 files changed, 26 insertions, 17 deletions
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 |