feat(connectedness): show that if f is n-connected, then trunc_functor k f is so, too

hott/algebra/order.hlean

@@ -40,8 +40,20 @@ end
 structure linear_weak_order [class] (A : Type) extends weak_order A :=
 (le_total : Πa b, le a b ⊎ le b a)
 
-definition le.total [s : linear_weak_order A] (a b : A) : a ≤ b ⊎ b ≤ a :=
-!linear_weak_order.le_total
+section
+  variables [linear_weak_order A]
+
+  theorem le.total (a b : A) : a ≤ b ⊎ b ≤ a := !linear_weak_order.le_total
+
+  theorem le_of_not_ge {a b : A} (H : ¬ a ≥ b) : a ≤ b := sum.resolve_left !le.total H
+
+  definition le_by_cases (a b : A) {P : Type} (H1 : a ≤ b → P) (H2 : b ≤ a → P) : P :=
+  begin
+    cases (le.total a b) with H H,
+    { exact H1 H},
+    { exact H2 H}
+  end
+end
 
 /- strict orders -/
 

hott/homotopy/connectedness.hlean

@@ -27,7 +27,7 @@ namespace is_conn
   theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A :=
   begin
     apply is_contr_equiv_closed,
-    apply trunc_trunc_equiv_left _ n k H
+    apply trunc_trunc_equiv_left _ H
   end
 
   theorem is_conn_fun_of_le {A B : Type} (f : A → B) {n k : ℕ₋₂} (H : n ≤ k)
@@ -244,14 +244,21 @@ namespace is_conn
   -- Corollary 7.5.5
   definition is_conn_homotopy (n : ℕ₋₂) {A B : Type} {f g : A → B}
     (p : f ~ g) (H : is_conn_fun n f) : is_conn_fun n g :=
-  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
+  @retract_of_conn_is_conn _ _
+    (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
 
   -- all types are -2-connected
   definition is_conn_minus_two (A : Type) : is_conn -2 A :=
-  is_trunc_trunc -2 A
+  _
+
+  -- the following trivial cases are solved by type class inference
+  definition is_conn_of_is_contr (k : ℕ₋₂) (A : Type) [is_contr A] : is_conn k A := _
+  definition is_conn_fun_of_is_equiv (k : ℕ₋₂) {A B : Type} (f : A → B) [is_equiv f] :
+    is_conn_fun k f :=
+  _
 
   -- Lemma 7.5.14
-  theorem is_equiv_trunc_functor_of_is_conn_fun {A B : Type} (n : ℕ₋₂) (f : A → B)
+  theorem is_equiv_trunc_functor_of_is_conn_fun [instance] {A B : Type} (n : ℕ₋₂) (f : A → B)
     [H : is_conn_fun n f] : is_equiv (trunc_functor n f) :=
   begin
     fapply adjointify,
@@ -265,7 +272,7 @@ namespace is_conn
     [H : is_conn_fun n f] : trunc n A ≃ trunc n B :=
   equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f)
 
-  definition is_conn_fun_trunc_functor {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : k ≤ n)
+  definition is_conn_fun_trunc_functor_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : k ≤ n)
     [H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) :=
   begin
     apply is_conn_fun.intro,
@@ -278,4 +285,20 @@ namespace is_conn
       induction a with a, esimp, rewrite [is_conn_fun.elim_β]}
   end
 
+  definition is_conn_fun_trunc_functor_of_ge {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k)
+    [H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) :=
+  begin
+    apply is_conn_fun_of_is_equiv,
+    apply is_equiv_trunc_functor_of_le f H
+  end
+
+  -- Exercise 7.18
+  definition is_conn_fun_trunc_functor {n k : ℕ₋₂} {A B : Type} (f : A → B)
+    [H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) :=
+  begin
+    eapply algebra.le_by_cases k n: intro H,
+    { exact is_conn_fun_trunc_functor_of_le f H},
+    { exact is_conn_fun_trunc_functor_of_ge f H}
+  end
+
 end is_conn

hott/types/trunc.hlean

@@ -11,7 +11,7 @@ Properties of trunc_index, is_trunc, trunctype, trunc, and the pointed versions
 import .pointed2 ..function algebra.order types.nat.order
 
 open eq sigma sigma.ops pi function equiv trunctype
-     is_equiv prod pointed nat is_trunc algebra
+     is_equiv prod pointed nat is_trunc algebra sum
 
   /- basic computation with ℕ₋₂, its operations and its order -/
 namespace trunc_index
@@ -64,13 +64,30 @@ namespace trunc_index
     { exfalso, apply @not_succ_le_self n, exact trunc_index.le_trans H1 H2}
   end
 
-  protected definition le_succ {n m : ℕ₋₂} (H1 : n ≤ m): n ≤ m.+1 :=
+  protected definition le_succ {n m : ℕ₋₂} (H1 : n ≤ m) : n ≤ m.+1 :=
   le.step H1
 
+  protected definition self_le_succ (n : ℕ₋₂) : n ≤ n.+1 :=
+  le.step (trunc_index.le.tr_refl n)
+
+  -- the order is total
+  protected theorem le_sum_le (n m : ℕ₋₂) : n ≤ m ⊎ m ≤ n :=
+  begin
+    induction m with m IH,
+    { exact inr !minus_two_le},
+    { cases IH with H H,
+      { exact inl (trunc_index.le_succ H)},
+      { cases H with n' H,
+        { exact inl !trunc_index.self_le_succ},
+        { exact inr (succ_le_succ H)}}}
+  end
+
 end trunc_index open trunc_index
 
-definition weak_order_trunc_index [trans_instance] [reducible] : weak_order trunc_index :=
-weak_order.mk le trunc_index.le.tr_refl @trunc_index.le_trans @trunc_index.le_antisymm
+definition linear_weak_order_trunc_index [trans_instance] [reducible] :
+  linear_weak_order trunc_index :=
+linear_weak_order.mk le trunc_index.le.tr_refl @trunc_index.le_trans @trunc_index.le_antisymm
+                     trunc_index.le_sum_le
 
 namespace trunc_index
 
@@ -198,6 +215,15 @@ namespace trunc_index
     exact le_of_succ_le_succ (le_of_succ_le_succ H)
   end
 
+  protected theorem succ_le_of_not_le {n m : ℕ₋₂} (H : ¬ n ≤ m) : m.+1 ≤ n :=
+  begin
+    cases (le.total n m) with H2 H2,
+    { exfalso, exact H H2},
+    { cases H2 with n' H2',
+      { exfalso, exact H !le.refl},
+      { exact succ_le_succ H2'}}
+  end
+
 end trunc_index open trunc_index
 
 namespace is_trunc
@@ -310,7 +336,7 @@ namespace is_trunc
   is_set_of_double_neg_elim (λa b, by_contradiction)
   end
 
-  theorem is_trunc_of_axiom_K_of_le {A : Type} (n : ℕ₋₂) (H : -1 ≤ n)
+  theorem is_trunc_of_axiom_K_of_le {A : Type} {n : ℕ₋₂} (H : -1 ≤ n)
     (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A :=
   @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_le H (λp, eq.rec_on p !K))
 
@@ -472,7 +498,7 @@ namespace trunc
   end
 
   /- equivalences between truncated types (see also hit.trunc) -/
-  definition trunc_trunc_equiv_left [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m)
+  definition trunc_trunc_equiv_left [constructor] (A : Type) {n m : ℕ₋₂} (H : n ≤ m)
     : trunc n (trunc m A) ≃ trunc n A :=
   begin
     note H2 := is_trunc_of_le (trunc n A) H,
@@ -483,7 +509,7 @@ namespace trunc
     { intro x, induction x with x, induction x with x, reflexivity}
   end
 
-  definition trunc_trunc_equiv_right [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m)
+  definition trunc_trunc_equiv_right [constructor] (A : Type) {n m : ℕ₋₂} (H : n ≤ m)
     : trunc m (trunc n A) ≃ trunc n A :=
   begin
     apply trunc_equiv,
@@ -492,7 +518,7 @@ namespace trunc
 
   definition trunc_equiv_trunc_of_le {n m : ℕ₋₂} {A B : Type} (H : n ≤ m)
     (f : trunc m A ≃ trunc m B) : trunc n A ≃ trunc n B :=
-  (trunc_trunc_equiv_left A _ _ H)⁻¹ᵉ ⬝e trunc_equiv_trunc n f ⬝e trunc_trunc_equiv_left B _ _ H
+  (trunc_trunc_equiv_left A H)⁻¹ᵉ ⬝e trunc_equiv_trunc n f ⬝e trunc_trunc_equiv_left B H
 
   definition trunc_trunc_equiv_trunc_trunc [constructor] (n m : ℕ₋₂) (A : Type)
     : trunc n (trunc m A) ≃ trunc m (trunc n A) :=
@@ -504,6 +530,27 @@ namespace trunc
     { reflexivity}
   end
 
+  theorem is_trunc_trunc_of_le (A : Type)
+    (n : ℕ₋₂) {m k : ℕ₋₂} (H : m ≤ k) [is_trunc n (trunc k A)] : is_trunc n (trunc m A) :=
+  begin
+    apply is_trunc_equiv_closed,
+    { apply trunc_trunc_equiv_left, exact H},
+  end
+
+  definition trunc_functor_homotopy_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k) :
+    to_fun (trunc_trunc_equiv_left B H) ∘
+    trunc_functor n (trunc_functor k f) ∘
+    to_fun (trunc_trunc_equiv_left A H)⁻¹ᵉ ~
+      trunc_functor n f :=
+  begin
+    intro x, induction x with x, reflexivity
+  end
+
+  definition is_equiv_trunc_functor_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k)
+    [is_equiv (trunc_functor k f)] : is_equiv (trunc_functor n f) :=
+  is_equiv_of_equiv_of_homotopy (trunc_equiv_trunc_of_le H (equiv.mk (trunc_functor k f) _))
+                                (trunc_functor_homotopy_of_le f H)
+
   /- trunc_functor preserves surjectivity -/
 
   definition is_surjective_trunc_functor {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_surjective f]
@@ -539,19 +586,19 @@ namespace trunc
     : ptrunc n X ≃* X :=
   pequiv_of_equiv (trunc_equiv n X) idp
 
-  definition ptrunc_ptrunc_pequiv_left [constructor] (A : Type*) (n m : ℕ₋₂) (H : n ≤ m)
+  definition ptrunc_ptrunc_pequiv_left [constructor] (A : Type*) {n m : ℕ₋₂} (H : n ≤ m)
     : ptrunc n (ptrunc m A) ≃* ptrunc n A :=
-  pequiv_of_equiv (trunc_trunc_equiv_left A n m H) idp
+  pequiv_of_equiv (trunc_trunc_equiv_left A H) idp
 
-  definition ptrunc_ptrunc_pequiv_right [constructor] (A : Type*) (n m : ℕ₋₂) (H : n ≤ m)
+  definition ptrunc_ptrunc_pequiv_right [constructor] (A : Type*) {n m : ℕ₋₂} (H : n ≤ m)
     : ptrunc m (ptrunc n A) ≃* ptrunc n A :=
-  pequiv_of_equiv (trunc_trunc_equiv_right A n m H) idp
+  pequiv_of_equiv (trunc_trunc_equiv_right A H) idp
 
   definition ptrunc_pequiv_ptrunc_of_le {n m : ℕ₋₂} {A B : Type*} (H : n ≤ m)
     (f : ptrunc m A ≃* ptrunc m B) : ptrunc n A ≃* ptrunc n B :=
-  (ptrunc_ptrunc_pequiv_left A _ _ H)⁻¹ᵉ* ⬝e*
+  (ptrunc_ptrunc_pequiv_left A H)⁻¹ᵉ* ⬝e*
   ptrunc_pequiv_ptrunc n f ⬝e*
-  ptrunc_ptrunc_pequiv_left B _ _ H
+  ptrunc_ptrunc_pequiv_left B H
 
   definition ptrunc_ptrunc_pequiv_ptrunc_ptrunc [constructor] (n m : ℕ₋₂) (A : Type*)
     : ptrunc n (ptrunc m A) ≃ ptrunc m (ptrunc n A) :=

library/algebra/order.lean

@@ -43,6 +43,13 @@ section
   theorem le.total (a b : A) : a ≤ b ∨ b ≤ a := !linear_weak_order.le_total
 
   theorem le_of_not_ge {a b : A} (H : ¬ a ≥ b) : a ≤ b := or.resolve_left !le.total H
+
+  theorem le_by_cases (a b : A) {P : Prop} (H1 : a ≤ b → P) (H2 : b ≤ a → P) : P :=
+  begin
+    cases (le.total a b) with H H,
+    { exact H1 H},
+    { exact H2 H}
+  end
 end
 
 /- strict orders -/