From 17c1b34bb9b4463203708196b14ac0f7e651cd3e Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= 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)) = + 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)) = + C -- 2.34.1