feat(library/hott): complete theorems about truncatedness of isomorphism sets

library/hott/algebra/category/basic.lean

@@ -14,17 +14,26 @@ structure category [class] (ob : Type) extends (precategory ob) :=
   (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
 
 namespace category
-  variables {ob : Type} (C : category ob) {a b : ob}
+  variables {ob : Type} {C : category ob} {a b : ob}
   include C
 
   -- Make iso_of_path_equiv a class instance
   -- TODO: Unsafe class instance?
   instance [persistent] iso_of_path_equiv
 
-  definition path_of_iso {a b : ob} : (Σ (f : hom a b), is_iso f) → a ≈ b :=
+  definition path_of_iso {a b : ob} : a ≅ b → a ≈ b :=
   iso_of_path⁻¹
 
-  definition ob_1_type : is_trunc 1 ob := sorry
+  definition foo {a b : ob} :
+
+  definition ob_1_type : is_trunc -2 .+1 .+1 .+1 ob :=
+  begin
+    apply is_trunc_succ, intros (a, b),
+    /-fapply trunc_equiv,
+      exact (@path_of_iso ob C a b),
+      apply inv_closed,
+    exact sorry,-/
+  end
 
 end category
 

library/hott/algebra/precategory/iso.lean

@@ -0,0 +1,68 @@
+-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Floris van Doorn, Jakob von Raumer
+
+import .basic .morphism hott.types.prod
+
+open path precategory sigma sigma.ops equiv is_equiv function truncation
+open prod
+
+namespace morphism
+  variables {ob : Type} [C : precategory ob] include C
+  variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
+
+  -- "is_iso f" is equivalent to a certain sigma type
+  definition sigma_equiv_of_is_iso (f : hom a b) :
+    (Σ (g : hom b a), (g ∘ f ≈ id) × (f ∘ g ≈ id)) ≃ is_iso f :=
+  begin
+    fapply (equiv.mk),
+      intro S, apply is_iso.mk,
+          exact (pr₁ S.2),
+        exact (pr₂ S.2),
+    fapply adjointify,
+        intro H, apply (is_iso.rec_on H), intros (g, η, ε),
+        exact (dpair g (pair η ε)),
+      intro H, apply (is_iso.rec_on H), intros (g, η, ε), apply idp,
+    intro S, apply (sigma.rec_on S), intros (g, ηε),
+    apply (prod.rec_on ηε), intros (η, ε), apply idp,
+  end
+
+  -- The structure for isomorphism can be characterized up to equivalence
+  -- by a sigma type.
+  definition sigma_is_iso_equiv ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
+  begin
+    fapply (equiv.mk),
+      intro S, apply isomorphic.mk, apply (S.2),
+      fapply adjointify,
+        intro p, apply (isomorphic.rec_on p), intros (f, H),
+        exact (dpair f H),
+      intro p, apply (isomorphic.rec_on p), intros (f, H), apply idp,
+    intro S, apply (sigma.rec_on S), intros (f, H), apply idp,
+  end
+
+  -- The statement "f is an isomorphism" is a mere proposition
+  definition is_hprop_of_is_iso : is_hset (is_iso f) :=
+  begin
+    apply trunc_equiv,
+      apply (equiv.to_is_equiv (!sigma_equiv_of_is_iso)),
+    apply sigma_trunc,
+      apply (!homH),
+    intro g, apply trunc_prod,
+      repeat (apply succ_is_trunc; apply trunc_succ; apply (!homH)),
+  end
+
+  -- The type of isomorphisms between two objects is a set
+  definition is_hset_iso : is_hset (a ≅ b) :=
+  begin
+    apply trunc_equiv,
+      apply (equiv.to_is_equiv (!sigma_is_iso_equiv)),
+    apply sigma_trunc,
+      apply homH,
+    intro f, apply is_hprop_of_is_iso,
+  end
+
+  -- In a precategory, equal objects are isomorphic
+  definition iso_of_path (p : a ≈ b) : isomorphic a b :=
+  path.rec_on p (isomorphic.mk id)
+
+end morphism

library/hott/algebra/precategory/morphism.lean

@@ -1,10 +1,10 @@
 -- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
+-- Authors: Floris van Doorn, Jakob von Raumer
 
-import .basic
+import .basic hott.types.sigma
 
-open path precategory sigma sigma.ops
+open path precategory sigma sigma.ops equiv is_equiv function truncation
 
 namespace morphism
   variables {ob : Type} [C : precategory ob] include C
@@ -130,26 +130,22 @@ namespace morphism
 
   namespace isomorphic
 
-    --open relation
+    -- openrelation
     instance [persistent] is_iso
 
-    theorem refl  (a     : ob)                           : isomorphic a a :=
+    definition refl (a : ob) : a ≅ a :=
     mk id
 
-    theorem symm  ⦃a b   : ob⦄ (H  : isomorphic a b)     : isomorphic b a :=
+    definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
     mk (inverse (iso H))
 
-    theorem trans ⦃a b c : ob⦄ (H1 : isomorphic a b) (H2 : isomorphic b c) : isomorphic a c :=
+    definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
     mk (iso H2 ∘ iso H1)
 
   --theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic :=
   --is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
   end isomorphic
 
-  -- In a precategory, equal objects are isomorphic
-  definition iso_of_path (p : a ≈ b) : isomorphic a b :=
-  path.rec_on p (isomorphic.mk id)
-
   inductive is_mono [class] (f : a ⟶ b) : Type :=
   mk : (∀c (g h : hom c a), f ∘ g ≈ f ∘ h → g ≈ h) → is_mono f
   inductive is_epi  [class] (f : a ⟶ b) : Type :=

library/hott/types/sigma.lean

@@ -11,6 +11,7 @@ import ..trunc .prod
 open path sigma sigma.ops equiv is_equiv
 
 namespace sigma
+  -- remove the ₁'s (globally)
   variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
@@ -50,9 +51,9 @@ namespace sigma
   definition dpair_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
       :  dpair (path_sigma p q)..1 (path_sigma p q)..2 ≈ ⟨p, q⟩ :=
   begin
-    reverts (p, q),
+    generalize q, generalize p,
     apply (destruct u), intros (u1, u2),
-    apply (destruct v), intros (v1, v2, p), generalize v2, --change to revert
+    apply (destruct v), intros (v1, v2, p), generalize v2,
     apply (path.rec_on p), intros (v2, q),
     apply (path.rec_on q), apply idp
   end
@@ -74,7 +75,7 @@ namespace sigma
   definition transport_pr1_path_sigma {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
       : transport (λx, B' x.1) (path_sigma p q) ≈ transport B' p :=
   begin
-    reverts (p, q),
+    generalize q, generalize p,
     apply (destruct u), intros (u1, u2),
     apply (destruct v), intros (v1, v2, p), generalize v2,
     apply (path.rec_on p), intros (v2, q),
@@ -120,7 +121,7 @@ namespace sigma
       path_sigma_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
     ≈ path_sigma_dpair p1 q1 ⬝ path_sigma_dpair  p2 q2 :=
   begin
-    reverts (b', p2, b'', q1, q2),
+    generalize q2, generalize q1, generalize b'', generalize p2, generalize b',
     apply (path.rec_on p1), intros (b', p2),
     apply (path.rec_on p2), intros (b'', q1),
     apply (path.rec_on q1), intro q2,
@@ -132,7 +133,7 @@ namespace sigma
       path_sigma (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
     ≈ path_sigma p1 q1 ⬝ path_sigma p2 q2 :=
   begin
-    reverts (p1, q1, p2, q2),
+    generalize q2, generalize p2, generalize q1, generalize p1,
     apply (destruct u), intros (u1, u2),
     apply (destruct v), intros (v1, v2),
     apply (destruct w), intros,
@@ -142,7 +143,7 @@ namespace sigma
   definition path_sigma_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
       path_sigma_dpair p q ≈ path_sigma_dpair p idp ⬝ path_sigma_dpair idp q :=
   begin
-    reverts (b', q),
+    generalize q, generalize b',
     apply (path.rec_on p), intros (b', q),
     apply (path.rec_on q), apply idp
   end
@@ -171,7 +172,7 @@ namespace sigma
               q2
               s
   -- begin
-  --   reverts (q2, s),
+  --   generalize s, generalize q2,
   --   apply (path.rec_on r), intros (q2, s),
   --   apply (path.rec_on s), apply idp
   -- end
@@ -180,7 +181,7 @@ namespace sigma
   /- A path between paths in a total space is commonly shown component wise. -/
   definition path_path_sigma {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
   begin
-    reverts (q, r, s),
+    generalize s, generalize r, generalize q,
     apply (path.rec_on p),
     apply (destruct u), intros (u1, u2, q, r, s),
     apply concat, rotate 1,
@@ -188,6 +189,7 @@ namespace sigma
     apply (path_path_sigma_path_sigma r s)
   end
 
+
   /- In Coq they often have to give u and v explicitly when using the following definition -/
   definition path_path_sigma_uncurried {p q : u ≈ v}
       (rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
@@ -221,7 +223,7 @@ namespace sigma
   definition transport_sigma_' {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a ≈ a')
       (bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd ≈ ⟨p ▹ bcd.1, p ▹ bcd.2.1, p ▹D2 bcd.2.2⟩ :=
   begin
-    revert bcd,
+    generalize bcd,
     apply (path.rec_on p), intro bcd,
     apply (destruct bcd), intros (b, cd),
     apply (destruct cd), intros (c, d),
@@ -234,35 +236,15 @@ namespace sigma
   definition functor_sigma (u : Σa, B a) : Σa', B' a' :=
   ⟨f u.1, g u.1 u.2⟩
 
-  -- variables {A A' : Type} {B : A → Type} {B' : A' → Type} (f : A → A') (g : Πa, B a → B' (f a))
-  --           (H1 : is_equiv f) (H2 : Π (a : A), is_equiv (g a)) (u' : Σ (a' : A'), B' a')
-  --           (a' : A') (b' : B' a')
-  -- check retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))) ≈ b'
-  -- check retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b')))
-  -- check (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b')))
-  -- check retr f a'
-
   /- Equivalences -/
-  irreducible inv --function.compose
+
-  --TODO: remove explicit arguments of IsEquiv
+  --remove explicit arguments of IsEquiv
   definition isequiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, @is_equiv (B a) (B' (f a)) (g a)]
       : is_equiv (functor_sigma f g) :=
-  adjointify (functor_sigma f g)
+  /-adjointify (functor_sigma f g)
-             (functor_sigma (f⁻¹) (λ(x : A') (y : B' x),
+             (functor_sigma (f⁻¹) (λ(x : A') (y : B' x), ((g (f⁻¹ x))⁻¹ ((retr f x)⁻¹ ▹ y))))
-               ((g (f⁻¹ x))⁻¹ (transport B' (retr f x)⁻¹ y))))
+             sorry-/
-  -- begin
+             sorry
-  --   intro u',
-  --   apply (destruct u'), intros (a', b'),
-  --   apply (path_sigma (retr f a')),
-  --   -- show retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))) ≈ b',
-  --   -- from sorry
-  --   -- exact (calc
-  --   --   retr f a' ▹ g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))
-  --   --          ≈ retr f a' ▹ ((retr f a')⁻¹ ▹ b') : {retr (g (f⁻¹ a')) _}
-  --   --      ... ≈ b' : transport_pV)
-  -- end
-             proof (λu', sorry) qed
-             proof (λu, sorry) qed
 
   definition equiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
   equiv.mk (functor_sigma f g) !isequiv_functor_sigma