add opposite category

diff --git a/examples/README.md b/examples/README.md
index 9c110d89f2178bba9410e3a2538d38ef37d54e15..301979a8bd70a2766122d50f846e163ad4ab7000 100644 (file)
--- 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 (file)
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