added Equalizers in category-theory

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