diff options
Diffstat (limited to 'examples/category-theory/Equalizer.gf')
| -rw-r--r-- | examples/category-theory/Equalizer.gf | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/examples/category-theory/Equalizer.gf b/examples/category-theory/Equalizer.gf new file mode 100644 index 000000000..f7c9becd9 --- /dev/null +++ b/examples/category-theory/Equalizer.gf @@ -0,0 +1,34 @@ +abstract Equalizer = Categories ** { + +cat Equalizer ({c} : Category) ({x,y,z} : El c) (f,g : Arrow x y) (e : Arrow z x) ; + +data equalizer : ({c} : Category) + -> ({x,y,z} : El c) + -> (f,g : Arrow x y) + -> (e : Arrow z x) + -> EqAr (comp f e) (comp g e) + -> Equalizer f g e ; + +fun idEqualizer : ({c} : Category) + -> ({x,y} : El c) + -> (f : Arrow x y) + -> Equalizer f f (id x) ; +def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ; + + +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) + -> EqAr (comp e f) (comp e g) + -> CoEqualizer e f g ; + +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) ; + +}
\ No newline at end of file |