From dfbc6ba9a33168885310eee8ed2f41845bb78537 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Mon, 15 Mar 2010 09:57:39 +0000
Subject: added Equalizers in category-theory

---
 examples/category-theory/Equalizer.gf | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 examples/category-theory/Equalizer.gf

(limited to 'examples/category-theory/Equalizer.gf')

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
-- 
cgit v1.2.3