diff options
| author | krasimir <krasimir@chalmers.se> | 2010-03-15 10:41:39 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-03-15 10:41:39 +0000 |
| commit | d7c68cdf27a5e4a6b9dc402ae5d49fdf85321715 (patch) | |
| tree | 0c036764c987b058b64d81833a84e88c3ceb3daf /examples | |
| parent | dfbc6ba9a33168885310eee8ed2f41845bb78537 (diff) | |
two theorems without proofs: every equalizer is monomorphism; every coequalizer is epimorphisms
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/category-theory/Equalizer.gf | 21 |
1 files changed, 18 insertions, 3 deletions
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 |