From abb0a2684f41dcc628914ef4ea330dfa472fd07f Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
Date: Mon, 20 Apr 2015 16:24:48 +0200
Subject: [PATCH] Add quotient example

---
 examples/quotient.ctt | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 examples/quotient.ctt

diff --git a/examples/quotient.ctt b/examples/quotient.ctt
new file mode 100644
index 0000000..9a172c0
--- /dev/null
+++ b/examples/quotient.ctt
@@ -0,0 +1,20 @@
+module quotient where
+
+import prelude
+
+-- Quotient A by R
+data Quot (A : U) (R : A -> A -> U) =
+    quot (a : A)
+  | identification (a b : A) (r : R a b) <i> [ (i = 0) -> quot a, (i = 1) -> quot b ]
+  | setTruncation (a b : Quot A R) (p q : Id (Quot A R) a b) <i j> 
+       [ (i = 0) -> p @ j
+       , (i = 1) -> q @ j
+       , (j = 0) -> a
+       , (j = 1) -> b ]
+
+identQuot (A : U) (R : A -> A -> U) (a b : A) (r : R a b)
+  : Id (Quot A R) (quot a) (quot b) = <i> identification {Quot A R} a b r @ i
+
+setQuot (A : U) (R : A -> A -> U) : set (Quot A R) =
+   \(a b : Quot A R) (p q : Id (Quot A R) a b) ->
+     <i j> setTruncation {Quot A R} a b p q @ i @ j
-- 
2.34.1