diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/category-theory/InitialAndTerminal.gf | 43 | ||||
| -rw-r--r-- | examples/category-theory/Morphisms.gf | 33 |
2 files changed, 49 insertions, 27 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 diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf index 1d7f7e05c..e5f21c925 100644 --- a/examples/category-theory/Morphisms.gf +++ b/examples/category-theory/Morphisms.gf @@ -1,6 +1,6 @@ abstract Morphisms = Categories ** { -cat Iso ({c} : Category) (x,y : El c) ; +cat Iso ({c} : Category) ({x,y} : El c) (Arrow x y) (Arrow y x) ; data iso : ({c} : Category) -> ({x,y} : El c) @@ -8,12 +8,23 @@ data iso : ({c} : Category) -> (g : Arrow y x) -> (EqAr (comp f g) (id y)) -> (EqAr (comp g f) (id x)) - -> Iso x y ; + -> Iso f g ; + +fun isoOp : ({c} : Category) + -> ({x,y} : El c) + -> ({f} : Arrow x y) + -> ({g} : Arrow y x) + -> Iso f g + -> Iso (opAr g) (opAr f) ; +def isoOp {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = + iso {Op c} (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ; fun iso2mono : ({c} : Category) -> ({x,y} : El c) - -> (Iso x y -> Mono x y) ; -def iso2mono {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) = + -> ({f} : Arrow x y) + -> ({g} : Arrow y x) + -> (Iso f g -> Mono f) ; +def iso2mono {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = mono f (\h,m,eq_fh_fm -> eqSym (eqTran (eqIdR m) -- h = m (eqTran (eqCompR id_gf m) -- id . m = h @@ -26,8 +37,10 @@ def iso2mono {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) = fun iso2epi : ({c} : Category) -> ({x,y} : El c) - -> (Iso x y -> Epi x y) ; -def iso2epi {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) = + -> ({f} : Arrow x y) + -> ({g} : Arrow y x) + -> (Iso f g -> Epi f) ; +def iso2epi {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = epi {c} {x} {y} f (\{z},h,m,eq_hf_mf -> eqSym (eqTran (eqIdL m) -- h = m (eqTran (eqCompL m id_fg) -- m . id = h @@ -38,21 +51,21 @@ def iso2epi {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) = (eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g -- h . f = m . f -cat Mono ({c} : Category) (x,y : El c) ; +cat Mono ({c} : Category) ({x,y} : El c) (Arrow x y) ; data mono : ({c} : Category) -> ({x,y} : El c) -> (f : Arrow x y) -> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m) - -> Mono x y ; + -> Mono f ; -cat Epi ({c} : Category) (x,y : El c) ; +cat Epi ({c} : Category) ({x,y} : El c) (Arrow x y) ; data epi : ({c} : Category) -> ({x,y} : El c) -> (f : Arrow x y) -> (({z} : El c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m) - -> Epi x y ; + -> Epi f ; }
\ No newline at end of file |