diff --git a/examples/category-theory/Equalizer.gf b/examples/category-theory/Equalizer.gf index f7c9becd9..051a19200 100644 --- a/examples/category-theory/Equalizer.gf +++ b/examples/category-theory/Equalizer.gf @@ -1,4 +1,4 @@ -abstract Equalizer = Categories ** { +abstract Equalizer = Morphisms ** { cat Equalizer ({c} : Category) ({x,y,z} : El c) (f,g : Arrow x y) (e : Arrow z x) ; @@ -15,13 +15,20 @@ fun idEqualizer : ({c} : Category) -> Equalizer f f (id x) ; def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ; +fun equalizer2mono : ({c} : Category) + -> ({x,y,z} : El c) + -> (f,g : Arrow x y) + -> (e : Arrow z x) + -> Equalizer f g e + -> Mono e ; +-- def equalizer2mono = ... cat CoEqualizer ({c} : Category) ({x,y,z} : El c) (e : Arrow y z) (f,g : Arrow x y) ; data coequalizer : ({c} : Category) -> ({x,y,z} : El c) - -> (f,g : Arrow x y) -> (e : Arrow y z) + -> (f,g : Arrow x y) -> EqAr (comp e f) (comp e g) -> CoEqualizer e f g ; @@ -29,6 +36,14 @@ fun idCoEqualizer : ({c} : Category) -> ({x,y} : El c) -> (f : Arrow x y) -> CoEqualizer (id y) f f ; -def idCoEqualizer {c} {x} {y} f = coequalizer f f (id y) (eqCompR (eqRefl (id y)) f) ; +def idCoEqualizer {c} {x} {y} f = coequalizer (id y) f f (eqCompR (eqRefl (id y)) f) ; + +fun coequalizer2epi : ({c} : Category) + -> ({x,y,z} : El c) + -> ({e} : Arrow y z) + -> ({f,g} : Arrow x y) + -> CoEqualizer e f g + -> Epi e ; +-- def coequalizer2epi = ... } \ No newline at end of file