feat(hott): prove HoTT book 7.5.4 and 7.5.5

hott/function.hlean

@@ -223,9 +223,17 @@ namespace function
 
   variable {f}
 
+  definition is_retraction_trunc_functor [instance] (r : A → B) [H : is_retraction r]
+    (n : trunc_index) : is_retraction (trunc_functor n r) :=
+  is_retraction.mk
+    (trunc_functor n (sect r))
+    (λb,
+      ((trunc_functor_compose n (sect r) r) b)⁻¹
+      ⬝ trunc_homotopy n (right_inverse r) b
+      ⬝ trunc_functor_id B n b)
+
   -- Lemma 3.11.7
-  definition is_contr_retract {A B : Type} (r : A → B) [H : is_retraction r]
-    : is_contr A → is_contr B :=
+  definition is_contr_retract (r : A → B) [H : is_retraction r] : is_contr A → is_contr B :=
   begin
     intro CA,
     apply is_contr.mk (r (center A)),

hott/homotopy/connectedness.hlean

@@ -9,7 +9,7 @@ open eq is_trunc is_equiv nat equiv trunc function
 
 namespace homotopy
 
-  definition is_conn (n : trunc_index) (A : Type) : Type :=
+  definition is_conn [reducible] (n : trunc_index) (A : Type) : Type :=
   is_contr (trunc n A)
 
   definition is_conn_map (n : trunc_index) {A B : Type} (f : A → B) : Type :=
@@ -38,10 +38,31 @@ namespace homotopy
     exact @center (∥fiber f b∥) (H b),
   end
 
-  definition merely_of_minus_one_conn {A : Type} : is_conn -1 A → ∥ A ∥ :=
+  definition merely_of_minus_one_conn {A : Type} : is_conn -1 A → ∥A∥ :=
   λH, @center (∥A∥) H
 
   definition minus_one_conn_of_merely {A : Type} : ∥A∥ → is_conn -1 A :=
   @is_contr_of_inhabited_hprop (∥A∥) (is_trunc_trunc -1 A)
 
+  section
+    open arrow
+
+    variables {f g : arrow}
+
+    -- Lemma 7.5.4
+    definition retract_of_conn_is_conn [instance] (r : arrow_hom f g) [H : is_retraction r]
+      (n : trunc_index) [K : is_conn_map n f] : is_conn_map n g :=
+    begin
+      intro b, unfold is_conn,
+      apply is_contr_retract (trunc_functor n (retraction_on_fiber r b)),
+      exact K (on_cod (arrow.is_retraction.sect r) b)
+    end
+
+  end
+
+  -- Corollary 7.5.5
+  definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B}
+    (p : f ~ g) (H : is_conn_map n f) : is_conn_map n g :=
+  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H 
+
 end homotopy

hott/types/arrow_2.hlean

@@ -18,6 +18,9 @@ namespace arrow
   abbreviation dom [unfold 2] := @arrow.dom
   abbreviation cod [unfold 2] := @arrow.cod
 
+  definition arrow_of_fn {A B : Type} (f : A → B) : arrow :=
+  arrow.mk A B f
+
   structure morphism (A B : Type) :=
     (mor : A → B)
 
@@ -90,3 +93,19 @@ namespace arrow
   end
 
 end arrow
+
+namespace arrow
+  variables {A B : Type} {f g : A → B} (p : f ~ g)
+
+  definition arrow_hom_of_homotopy : arrow_hom (arrow_of_fn f) (arrow_of_fn g) :=
+  arrow_hom.mk id id (λx, (p x)⁻¹)
+
+  definition is_retraction_arrow_hom_of_homotopy [instance]
+    : is_retraction (arrow_hom_of_homotopy p) :=
+  is_retraction.mk
+    (arrow_hom_of_homotopy (λx, (p x)⁻¹))
+    (λa, idp)
+    (λb, idp)
+    (λa, con_eq_of_eq_inv_con (ap_id _))
+
+end arrow