From 61287f39259bdca55ba9874d369d2d2191bb1baf Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Mon, 15 Feb 2010 10:35:24 +0000
Subject: more category theory -> morphisms, initial and terminal objects

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

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

diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
new file mode 100644
index 000000000..7ac7b0864
--- /dev/null
+++ b/examples/category-theory/InitialAndTerminal.gf
@@ -0,0 +1,35 @@
+abstract InitialAndTerminal = Morphisms ** {
+
+cat  Initial  (c : Category) ;
+data initial  : ({c} : Category)
+              -> (x : El c)
+              -> ((y : El c) -> Arrow x y)
+              -> Initial c ;
+
+fun initEl : ({c} : Category)
+              -> Initial c
+              -> El c ;
+def initEl (initial x f) = x ;
+
+fun initials2iso :  ({c} : Category)
+                 -> ({x,y} : Initial c)
+                 -> Iso (initEl x) (initEl y) ;
+-- def initials2iso = .. ;
+
+cat  Terminal (c : Category) ;
+data terminal : ({c} : Category)
+              -> (y : El c)
+              -> ((x : El c) -> Arrow x y)
+              -> Terminal c ;
+
+fun termEl : ({c} : Category)
+             -> Terminal c
+             -> El c ;
+def termEl (terminal x f) = x ;
+
+fun terminals2iso :  ({c} : Category)
+                  -> ({x,y} : Terminal c)
+                  -> Iso (termEl x) (termEl y) ;
+-- def terminals2iso = .. ;
+
+}
\ No newline at end of file
-- 
cgit v1.2.3