diff options
| -rw-r--r-- | examples/category-theory/CategoryTheory.gf | 2 | ||||
| -rw-r--r-- | examples/category-theory/Equalizer.gf | 34 |
2 files changed, 35 insertions, 1 deletions
diff --git a/examples/category-theory/CategoryTheory.gf b/examples/category-theory/CategoryTheory.gf index d75f71694..800bdb4a3 100644 --- a/examples/category-theory/CategoryTheory.gf +++ b/examples/category-theory/CategoryTheory.gf @@ -3,6 +3,6 @@ abstract CategoryTheory , Morphisms
, InitialAndTerminal
, Functor
-
+ , Equalizer
** {
}
\ No newline at end of file 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 |