msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

two theorems without proofs: every equalizer is monomorphism; every coequalizer is epimorphisms

Browse Source
This commit is contained in:
krasimir
2010-03-15 10:41:39 +00:00
parent dfbc6ba9a3
commit d7c68cdf27
1 changed files with 18 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
examples/category-theory/Equalizer.gf
View File

@@ -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) ; 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) ; -> Equalizer f f (id x) ;
def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (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) ; cat CoEqualizer ({c} : Category) ({x,y,z} : El c) (e : Arrow y z) (f,g : Arrow x y) ;
data coequalizer : ({c} : Category) data coequalizer : ({c} : Category)
-> ({x,y,z} : El c) -> ({x,y,z} : El c)
-> (f,g : Arrow x y)
-> (e : Arrow y z) -> (e : Arrow y z)
-> (f,g : Arrow x y)
-> EqAr (comp e f) (comp e g) -> EqAr (comp e f) (comp e g)
-> CoEqualizer e f g ; -> CoEqualizer e f g ;
@@ -29,6 +36,14 @@ fun idCoEqualizer : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
-> (f : Arrow x y) -> (f : Arrow x y)
-> CoEqualizer (id y) f f ; -> 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 = ...
} }