From df73931a6dfd9501d2d9bbf2e782b3c21d734c24 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 25 Sep 2015 17:36:35 -0400
Subject: [PATCH] feat(category.opposite): prove that the opposite of a
 univalent category is univalent

---
 .../category/constructions/opposite.hlean     | 46 ++++++++++++++++++-
 hott/algebra/category/iso.hlean               |  4 ++
 hott/algebra/category/limits.hlean            | 11 +++--
 3 files changed, 55 insertions(+), 6 deletions(-)

diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean
index 32ab9f087..6b5d193c5 100644
--- a/hott/algebra/category/constructions/opposite.hlean
+++ b/hott/algebra/category/constructions/opposite.hlean
@@ -8,7 +8,7 @@ Opposite precategory and (TODO) category
 
 import ..functor ..category
 
-open eq functor
+open eq functor iso equiv is_equiv
 
 namespace category
 
@@ -50,4 +50,48 @@ namespace category
 
   postfix `ᵒᵖ`:(max+2) := opposite_functor
 
+  definition opposite_iso [constructor] {ob : Type} [C : precategory ob] {a b : ob}
+    (H : @iso _ C a b) : @iso _ (opposite C) a b :=
+  begin
+    fapply @iso.MK,
+    { exact to_inv H},
+    { exact to_hom H},
+    { exact to_left_inverse  H},
+    { exact to_right_inverse H},
+  end
+
+  definition iso_of_opposite_iso [constructor]  {ob : Type} [C : precategory ob] {a b : ob}
+    (H : @iso _ (opposite C) a b) : @iso _ C a b :=
+  begin
+    fapply iso.MK,
+    { exact to_inv H},
+    { exact to_hom H},
+    { exact to_left_inverse  H},
+    { exact to_right_inverse H},
+  end
+
+  definition opposite_iso_equiv [constructor]  {ob : Type} [C : precategory ob] (a b : ob)
+    : @iso _ (opposite C) a b ≃ @iso _ C a b :=
+  begin
+    fapply equiv.MK,
+    { exact iso_of_opposite_iso},
+    { exact opposite_iso},
+    { intro H, apply iso_eq, reflexivity},
+    { intro H, apply iso_eq, reflexivity},
+  end
+
+  definition is_univalent_opposite (C : Category) : is_univalent (Opposite C) :=
+  begin
+    intro x y,
+    fapply is_equiv_of_equiv_of_homotopy,
+    { refine @eq_equiv_iso C C x y ⬝e _, symmetry, apply opposite_iso_equiv},
+    { intro p, induction p, reflexivity}
+  end
+
+  definition category_opposite [constructor] (C : Category) : category (Opposite C) :=
+  category.mk _ (is_univalent_opposite C)
+
+  definition Category_opposite [constructor] (C : Category) : Category :=
+  Category.mk _ (category_opposite C)
+
 end category
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 840c231f0..64b4be25e 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -145,12 +145,14 @@ namespace iso
     (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
   @(mk f) (is_iso.mk H1 H2)
 
+  variable {C}
   definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹
   definition to_left_inverse  [unfold 5] (f : a ≅ b) : (to_hom f)⁻¹ ∘ (to_hom f) = id :=
   left_inverse  (to_hom f)
   definition to_right_inverse [unfold 5] (f : a ≅ b) : (to_hom f) ∘ (to_hom f)⁻¹ = id :=
   right_inverse (to_hom f)
 
+  variable [C]
   protected definition refl [constructor] (a : ob) : a ≅ a :=
   mk (ID a)
 
@@ -167,8 +169,10 @@ namespace iso
       : iso.mk f = iso.mk f' :=
   apd011 iso.mk p !is_hprop.elim
 
+  variable {C}
   definition iso_eq {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' :=
   by (cases f; cases f'; apply (iso_mk_eq p))
+  variable [C]
 
   -- The structure for isomorphism can be characterized up to equivalence by a sigma type.
   protected definition sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean
index db1e0c320..8efa171cc 100644
--- a/hott/algebra/category/limits.hlean
+++ b/hott/algebra/category/limits.hlean
@@ -41,15 +41,16 @@ namespace category
 
   structure has_terminal_object [class] (D : Precategory) :=
     (d : D)
-    (is_term : is_terminal d)
+    (is_terminal : is_terminal d)
 
-  abbreviation terminal_object [constructor] := @has_terminal_object.d
-  attribute has_terminal_object.is_term [instance]
+  definition terminal_object [reducible] [unfold 2] := @has_terminal_object.d
+  attribute has_terminal_object.is_terminal [instance]
 
   variable {D}
   definition terminal_object_iso_terminal_object (H₁ H₂ : has_terminal_object D)
     : @terminal_object D H₁ ≅ @terminal_object D H₂ :=
-  terminal_iso_terminal (@has_terminal_object.is_term D H₁) (@has_terminal_object.is_term D H₂)
+  terminal_iso_terminal (@has_terminal_object.is_terminal D H₁)
+                        (@has_terminal_object.is_terminal D H₂)
 
   theorem is_hprop_has_terminal_object [instance] (D : Category)
     : is_hprop (has_terminal_object D) :=
@@ -96,7 +97,7 @@ namespace category
   definition limit_cone : cone F := !terminal_object
 
   definition is_terminal_limit_cone [instance] : is_terminal (limit_cone F) :=
-  has_terminal_object.is_term _
+  has_terminal_object.is_terminal _
 
   definition limit_object : D :=
   cone_obj.c (limit_cone F)