From 17c1b34bb9b4463203708196b14ac0f7e651cd3e Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Sun, 25 Dec 2016 22:30:29 +0100
Subject: [PATCH] add opposite category

---
 examples/README.md    |  3 +++
 examples/opposite.ctt | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 examples/opposite.ctt

diff --git a/examples/README.md b/examples/README.md
index 9c110d8..301979a 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -69,6 +69,9 @@ cubicaltt. The files contain:
 
 * **ordinal.ctt** - Ordinals.
 
+* **opposite.ctt** - Opposite category and a proof that C^op^op = C
+                     definitionally.
+
 * **pi.ctt** - Characterization of equality in pi types.
 
 * **prelude.ctt** - The prelude. Definition of Path types and basic
diff --git a/examples/opposite.ctt b/examples/opposite.ctt
new file mode 100644
index 0000000..6c01312
--- /dev/null
+++ b/examples/opposite.ctt
@@ -0,0 +1,35 @@
+-- Definition of the opposite category and verification that C^op^op = C definitionally
+module opposite where
+
+import category
+
+oppCat (C : precategory) : precategory = (Copp,isPrecategoryCopp)
+  where
+  A : U = cA C
+  homOpp (a b : A) : U = cH C b a
+
+  Copp : categoryData = (A,homOpp)
+  idOpp (a : A) : homOpp a a = C.2.1 a
+  compOpp (a b c : A) (f : homOpp a b) (g : homOpp b c) : homOpp a c =
+    C.2.2.1 c b a g f
+
+  homOppSet (a b : A) : set (homOpp a b) = cHSet C b a
+
+  left_id (a b : A) (f : homOpp a b) :
+    Path (homOpp a b) (compOpp a a b (idOpp a) f) f = cPathR C b a f
+
+  right_id (a b : A) (f : homOpp a b) :
+    Path (homOpp a b) (compOpp a b b f (idOpp b)) f = cPathL C b a f
+
+  assoc (a b c d : A) (f : homOpp a b) (g : homOpp b c) (h : homOpp c d) :
+    Path (homOpp a d) (compOpp a c d (compOpp a b c f g) h)
+                      (compOpp a b d f (compOpp b c d g h)) =
+      <i> cPathC C d c b a h g f @ -i
+
+  isPrecategory2Copp : isPrecategory2 Copp idOpp compOpp =
+    (homOppSet,left_id,right_id,assoc)
+
+  isPrecategoryCopp : isPrecategory Copp = (idOpp,compOpp,isPrecategory2Copp)
+
+oppOppCat (C : precategory) : Path precategory C (oppCat (oppCat C)) =
+  <i> C
-- 
2.34.1