From 099bd95ebd3b46d8a715152c9252fbc75eb96d08 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 25 Sep 2015 16:25:46 -0400
Subject: [PATCH] feat(category.limits): prove that being complete is a mere
 proposition for categories

---
 .../algebra/category/constructions/cone.hlean | 95 ++++++++++++++++++-
 .../algebra/category/constructions/hset.hlean |  4 +-
 hott/algebra/category/limits.hlean            | 10 ++
 3 files changed, 105 insertions(+), 4 deletions(-)

diff --git a/hott/algebra/category/constructions/cone.hlean b/hott/algebra/category/constructions/cone.hlean
index 5d034e382..5cb0c872f 100644
--- a/hott/algebra/category/constructions/cone.hlean
+++ b/hott/algebra/category/constructions/cone.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn
 Cones
 -/
 
-import ..nat_trans
+import ..nat_trans ..category
 
-open functor nat_trans eq equiv is_trunc
+open functor nat_trans eq equiv is_trunc is_equiv iso sigma sigma.ops pi
 
 namespace category
 
@@ -37,6 +37,20 @@ namespace category
     : is_hprop (f = g) :=
   _
 
+  definition cone_obj_eq (p : cone_obj.c x = cone_obj.c y)
+    (q : Πi, cone_obj.η x i = cone_obj.η y i ∘ hom_of_eq p) : x = y :=
+  begin
+    induction x, induction y, esimp at *, induction p, apply ap (cone_obj.mk c),
+    apply nat_trans_eq, intro i, exact q i ⬝ !id_right
+  end
+
+  theorem c_cone_obj_eq (p : cone_obj.c x = cone_obj.c y)
+    (q : Πi, cone_obj.η x i = cone_obj.η y i ∘ hom_of_eq p) : ap cone_obj.c (cone_obj_eq p q) = p :=
+  begin
+    induction x, induction y, esimp at *, induction p,
+    esimp [cone_obj_eq], rewrite [-ap_compose,↑function.compose,ap_constant]
+  end
+
   theorem cone_hom_eq {f f' : cone_hom x y} (q : cone_hom.f f = cone_hom.f f') : f = f' :=
   begin
     induction f, induction f', esimp at *, induction q, apply ap (cone_hom.mk f),
@@ -70,4 +84,81 @@ namespace category
   definition cone [constructor] : Precategory :=
   precategory.Mk (precategory_cone F)
 
+  variable {F}
+  definition cone_iso_pr1 (h : x ≅ y) : cone_obj.c x ≅ cone_obj.c y :=
+  iso.MK
+    (cone_hom.f (to_hom h))
+    (cone_hom.f (to_inv h))
+    (ap cone_hom.f (to_left_inverse h))
+    (ap cone_hom.f (to_right_inverse h))
+
+
+  definition cone_iso.mk (f : cone_obj.c x ≅ cone_obj.c y)
+    (p : Πi, cone_obj.η y i ∘ to_hom f = cone_obj.η x i) : x ≅ y :=
+  begin
+    fapply iso.MK,
+    { exact !cone_hom.mk p},
+    { fapply cone_hom.mk,
+      { exact to_inv f},
+      { intro i, apply comp_inverse_eq_of_eq_comp, exact (p i)⁻¹}},
+    { apply cone_hom_eq, esimp, apply left_inverse},
+    { apply cone_hom_eq, esimp, apply right_inverse},
+  end
+
+  variables (x y)
+  definition cone_iso_equiv [constructor] : (x ≅ y) ≃ Σ(f : cone_obj.c x ≅ cone_obj.c y),
+                                          Πi, cone_obj.η y i ∘ to_hom f = cone_obj.η x i :=
+  begin
+    fapply equiv.MK,
+    { intro h, exact ⟨cone_iso_pr1 h, cone_hom.p (to_hom h)⟩},
+    { intro v, exact cone_iso.mk v.1 v.2},
+    { intro v, induction v with f p, fapply sigma_eq: esimp,
+      { apply iso_eq, reflexivity},
+      { apply is_hprop.elimo, apply is_trunc_pi, intro i, apply is_hprop_hom_eq}},
+    { intro h, esimp, apply iso_eq, apply cone_hom_eq, reflexivity},
+  end
+
+  --set_option pp.implicit true
+  definition cone_eq_equiv : (x = y) ≃ Σ(f : cone_obj.c x = cone_obj.c y),
+                                          Πi, cone_obj.η y i ∘ hom_of_eq f = cone_obj.η x i :=
+  begin
+    fapply equiv.MK,
+    { intro r, fapply sigma.mk, exact ap cone_obj.c r, induction r, intro i, apply id_right},
+    { intro v, induction v with p q, induction x with c η, induction y with c' η', esimp at *,
+      apply cone_obj_eq p, esimp, intro i, exact (q i)⁻¹},
+    { intro v, induction v with p q, induction x with c η, induction y with c' η', esimp at *,
+      induction p, esimp, fapply sigma_eq: esimp,
+      { apply c_cone_obj_eq},
+      { apply is_hprop.elimo, apply is_trunc_pi, intro i, apply is_hprop_hom_eq}},
+    { intro r, induction r, esimp, induction x, esimp, apply ap02, apply is_hprop.elim},
+  end
+
+  section is_univalent
+
+    definition is_univalent_cone {I : Precategory} {C : Category} (F : I ⇒ C)
+      : is_univalent (cone F) :=
+    begin
+      intro x y,
+      fapply is_equiv_of_equiv_of_homotopy,
+      { exact calc
+(x = y) ≃ (Σ(f : cone_obj.c x = cone_obj.c y), Πi, cone_obj.η y i ∘ hom_of_eq f = cone_obj.η x i)
+                  : cone_eq_equiv
+    ... ≃ (Σ(f : cone_obj.c x ≅ cone_obj.c y), Πi, cone_obj.η y i ∘ to_hom f = cone_obj.η x i)
+                  : sigma_equiv_sigma !eq_equiv_iso (λa, !equiv.refl)
+    ... ≃ (x ≅ y) : cone_iso_equiv },
+      { intro p, induction p, esimp [equiv.trans,equiv.symm], esimp [sigma_functor],
+        apply iso_eq, reflexivity}
+    end
+
+    definition category_cone [instance] [constructor] {I : Precategory} {C : Category} (F : I ⇒ C)
+      : category (cone_obj F) :=
+    category.mk _ (is_univalent_cone F)
+
+    definition Category_cone [constructor] {I : Precategory} {C : Category} (F : I ⇒ C)
+      : Category :=
+    Category.mk _ (category_cone F)
+
+  end is_univalent
+
+
 end category
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean
index a7edce766..16d9ba077 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/constructions/hset.hlean
@@ -99,7 +99,7 @@ namespace category
   local attribute Category.to.precategory [unfold 1]
   local attribute category.to_precategory [unfold 2]
 
-  definition is_complete_cone.{u v w} [constructor]
+  definition is_complete_set_cone.{u v w} [constructor]
     (I : Precategory.{v w}) (F : I ⇒ set.{max u v w}) : cone_obj F :=
   begin
   fapply cone_obj.mk,
@@ -120,7 +120,7 @@ namespace category
   definition is_complete_set.{u v w} : is_complete.{(max u v w)+1 (max u v w) v w} set :=
   begin
     intro I F, fapply has_terminal_object.mk,
-    { exact is_complete_cone.{u v w} I F},
+    { exact is_complete_set_cone.{u v w} I F},
     { intro c, esimp at *, induction c with X η, induction η with η p, esimp at *,
       fapply is_contr.mk,
       { fapply cone_hom.mk,
diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean
index 136e01d25..db1e0c320 100644
--- a/hott/algebra/category/limits.hlean
+++ b/hott/algebra/category/limits.hlean
@@ -75,6 +75,16 @@ namespace category
   definition has_limits_of_shape_of_is_complete [instance] [H : is_complete D] (I : Precategory)
     : has_limits_of_shape D I := H I
 
+  section
+    open pi
+    theorem is_hprop_has_limits_of_shape [instance] (D : Category) (I : Precategory)
+      : is_hprop (has_limits_of_shape D I) :=
+    by apply is_trunc_pi; intro F; exact is_hprop_has_terminal_object (Category_cone F)
+
+    local attribute is_complete [reducible]
+    theorem is_hprop_is_complete [instance] (D : Category) : is_hprop (is_complete D) := _
+  end
+
   variables {I D}
   definition has_terminal_object_cone [H : has_limits_of_shape D I]
     (F : I ⇒ D) : has_terminal_object (cone F) := H F