From 25adc81550e931f6ec55521ec575afae4e846931 Mon Sep 17 00:00:00 2001 From: krasimir Date: Sat, 20 Feb 2010 16:37:23 +0000 Subject: [PATCH] two theorems every iso is mono and every iso is epi --- examples/category-theory/Morphisms.gf | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf index 426419cc0..1d7f7e05c 100644 --- a/examples/category-theory/Morphisms.gf +++ b/examples/category-theory/Morphisms.gf @@ -13,16 +13,30 @@ data iso : ({c} : Category) fun iso2mono : ({c} : Category) -> ({x,y} : El c) -> (Iso x y -> Mono x y) ; --- def iso2mono (iso f g eq_fg eq_gf) = (mono f (\h m eq_fh_fm -> ...)) - --- eqIdR (eqTran eq_gf (eqComp g f h)) : EqAr (comp g (comp f h)) h --- comp g (comp f m) +def iso2mono {c} {x} {y} (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 + (eqTran (eqAssoc g f m) -- (g . f) . m = h + (eqSym (eqTran (eqIdR h) -- g . (f . m) = h + (eqTran (eqCompR id_gf h) -- id . h = g . (f . m) + (eqTran (eqAssoc g f h) -- (g . f) . h = g . (f . m) + (eqCompL g eq_fh_fm))))))))) ; -- g . (f . h) = g . (f . m) + -- f . h = f . m fun iso2epi : ({c} : Category) -> ({x,y} : El c) -> (Iso x y -> Epi x y) ; --- def iso2epi (iso f g eq_fg eq_gf) = (epi f (\h m eq_hf_mf -> ...)) - +def iso2epi {c} {x} {y} (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 + (eqTran (eqSym (eqAssoc m f g)) -- m . (f . g) = h + (eqSym (eqTran (eqIdL h) -- (m . f) . g = h + (eqTran (eqCompL h id_fg) -- h . id = (m . f) . g + (eqTran (eqSym (eqAssoc h f g)) -- h . (f . g) = (m . f) . g + (eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g + -- h . f = m . f cat Mono ({c} : Category) (x,y : El c) ;