feat(types/pointed): change definition of loop space

hott/homotopy/sphere.hlean

@@ -98,8 +98,10 @@ namespace sphere
   pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv
 
   definition surf {n : ℕ} : Ω[n] S. n :=
-  nat.rec_on n (by esimp [Iterated_loop_space]; exact base)
-               (by intro n s;exact apn n (equator n) s)
+  nat.rec_on n (proof base qed)
+               (begin intro m s, refine cast _ (apn m (equator m) s),
+                      exact ap Pointed.carrier !loop_space_succ_eq_in⁻¹ end)
+
 
   definition bool_of_sphere : S 0 → bool :=
   susp.rec ff tt (λx, empty.elim x)
@@ -120,12 +122,20 @@ namespace sphere
   definition sphere_eq_bool_pointed : S. 0 = Bool :=
   Pointed_eq sphere_equiv_bool idp
 
+  -- TODO: the commented-out part makes the forward function below "apn _ surf"
   definition pmap_sphere (A : Pointed) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A :=
   begin
-    revert A, induction n with n IH,
-    { intro A, rewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv},
-    { intro A, transitivity _, apply susp_adjoint_loop (S. n) A, apply IH}
-  end -- can we prove this in such a way that the function from left to right is apn _ surf?
+    -- fapply equiv_change_fun,
+    -- {
+      revert A, induction n with n IH: intro A,
+      { rewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv},
+      { refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e _, rewrite [loop_space_succ_eq_in]}
+    -- },
+    -- { intro f, exact apn n f surf},
+    -- { revert A, induction n with n IH: intro A f,
+    --   { exact sorry},
+    --   { exact sorry}}
+  end
 
   protected definition elim {n : ℕ} {P : Pointed} (p : Ω[n] P) : map₊ (S. n) P :=
   to_inv !pmap_sphere p

hott/init/equiv.hlean

@@ -287,7 +287,7 @@ namespace equiv
   protected definition trans [trans] (f : A ≃ B) (g : B ≃ C) : A ≃ C :=
   equiv.mk (g ∘ f) !is_equiv_compose
 
-  infixl `⬝e`:75 := equiv.trans
+  infixl ` ⬝e `:75 := equiv.trans
   postfix [parsing_only] `⁻¹ᵉ`:(max + 1) := equiv.symm
     -- notation for inverse which is not overloaded
   abbreviation erfl [constructor] := @equiv.refl

hott/init/logic.hlean

@@ -181,6 +181,9 @@ namespace iff
   definition rfl {a : Type} : a ↔ a :=
   refl a
 
+  definition iff_of_eq (a b : Type) (p : a = b) : a ↔ b :=
+  eq.rec rfl p
+
   definition trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c :=
   intro
     (assume Ha, elim_left H₂ (elim_left H₁ Ha))

hott/init/trunc.hlean

@@ -49,6 +49,7 @@ namespace is_trunc
   definition succ_le_succ {n m : trunc_index} (H : n ≤ m) : n.+1 ≤ m.+1 := H
   definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := H
   definition minus_two_le (n : trunc_index) : -2 ≤ n := star
+  definition le.refl (n : trunc_index) : n ≤ n := by induction n with n IH; exact star; exact IH
   definition empty_of_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := H
   end trunc_index
   definition trunc_index.of_nat [coercion] [reducible] (n : nat) : trunc_index :=

hott/types/pointed.hlean

@@ -6,7 +6,7 @@ Authors: Jakob von Raumer, Floris van Doorn
 Ported from Coq HoTT
 -/
 
-import arity .eq .bool .unit .sigma
+import arity .eq .bool .unit .sigma .nat.basic
 open is_trunc eq prod sigma nat equiv option is_equiv bool unit
 
 structure pointed [class] (A : Type) :=
@@ -66,12 +66,9 @@ namespace pointed
   definition Loop_space [reducible] [constructor] (A : Type*) : Type* :=
   pointed.mk' (point A = point A)
 
-  -- definition Iterated_loop_space : Type* → ℕ → Type*
-  -- | Iterated_loop_space A 0 := A
-  -- | Iterated_loop_space A (n+1) := Iterated_loop_space (Loop_space A) n
-
-  definition Iterated_loop_space [unfold 1] [reducible] (n : ℕ) (A : Type*) : Type* :=
-  nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A
+  definition Iterated_loop_space [unfold 1] [reducible] : ℕ → Type* → Type*
+  | Iterated_loop_space  0    X := X
+  | Iterated_loop_space (n+1) X := Loop_space (Iterated_loop_space n X)
 
   prefix `Ω`:(max+5) := Loop_space
   notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A
@@ -183,12 +180,6 @@ namespace pointed
       { esimp, exact !con.left_inv⁻¹}},
   end
 
-  -- definition Loop_space_functor (f : A →* B) : Ω A →* Ω B :=
-  -- begin
-  --   fapply pmap.mk,
-  --   { intro p, exact ap f p},
-  -- end
-
   -- set_option pp.notation false
   -- definition pmap_equiv_right (A : Type*) (B : Type)
   --   : (Σ(b : B), map₊ A (pointed.Mk b)) ≃ (A → B) :=
@@ -217,17 +208,59 @@ namespace pointed
       { esimp, exact !con.left_inv⁻¹}},
   end
 
+  definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B :=
+  begin
+    fconstructor,
+    { intro p, exact !respect_pt⁻¹ ⬝ ap f p ⬝ !respect_pt},
+    { esimp, apply con.left_inv}
+  end
+
   definition apn [unfold 3] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B :=
   begin
-  revert A B f, induction n with n IH,
-  { intros A B f, exact f},
-  { intros A B f, esimp, apply IH (Ω A),
-    { esimp, fconstructor,
-        intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt,
-        esimp, apply con.left_inv}}
+  induction n with n IH,
+  { exact f},
+  { esimp [Iterated_loop_space], exact ap1 IH}
+  end
+
+  variable (A)
+  definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) :=
+  begin
+    induction n with n IH,
+    { reflexivity},
+    { exact ap Loop_space IH}
+  end
+
+  definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) = Ω[m+n] (A) :=
+  begin
+    induction n with n IH,
+    { reflexivity},
+    { exact ap Loop_space IH}
+  end
+
+  definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A)  :=
+  idp
+
+  variable {A}
+  definition loop_space_loop_irrel (p : point A = point A) : Ω(Pointed.mk p) = Ω[2] A :=
+  begin
+    intros, fapply Pointed_eq,
+    { esimp, transitivity _,
+      apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹),
+      esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv},
+    { esimp, apply con.left_inv}
   end
 
-  definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := apn (succ 0) f
+  definition iterated_loop_space_loop_irrel (n : ℕ) (p : point A = point A)
+    : Ω[succ n](Pointed.mk p) = Ω[succ (succ n)] A :> Pointed :=
+  calc
+    Ω[succ n](Pointed.mk p) = Ω[n](Ω (Pointed.mk p)) : loop_space_succ_eq_in
+      ... = Ω[n] (Ω[2] A)                            : loop_space_loop_irrel
+      ... = Ω[2+n] A                                 : loop_space_add
+      ... = Ω[n+2] A                                 : add.comm
+
+  -- TODO:
+  -- definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f :=
+  -- _
 
   definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
   begin

hott/types/trunc.hlean

@@ -138,31 +138,27 @@ namespace is_trunc
     induction p, apply Hp
   end
 
+  theorem is_hprop_iff_is_contr {A : Type} (a : A) :
+    is_hprop A ↔ is_contr A :=
+  iff.intro (λH, is_contr.mk a (is_hprop.elim a)) _
+
   theorem is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) :
     is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) :=
   iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn)
-
+--set_option pp.all true
   theorem is_trunc_iff_is_contr_loop_succ (n : ℕ) (A : Type)
     : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](Pointed.mk a)) :=
   begin
     revert A, induction n with n IH,
-      { intros, esimp [Iterated_loop_space], apply iff.intro,
-        { intros H a, apply is_contr.mk idp, apply is_hprop.elim},
-        { intro H, apply is_hset_of_axiom_K, intros, apply is_hprop.elim}},
-      { intros, transitivity _, apply @is_trunc_succ_iff_is_trunc_loop n, constructor,
-        apply iff.pi_iff_pi, intros,
-        transitivity _, apply IH,
-        assert H : Πp : a = a, Ω(Pointed.mk p) = Ω(Pointed.mk (idpath a)),
-        { intros, fapply Pointed_eq,
-          { esimp, transitivity _,
-            apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹),
-            esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv},
-          { esimp, apply con.left_inv}},
-        transitivity _,
-          apply iff.pi_iff_pi, intro p,
-          rewrite [↑Iterated_loop_space,H],
-          apply iff.refl,
-        apply iff.imp_iff, reflexivity}
+    { intro A, esimp [Iterated_loop_space], transitivity _,
+      { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl},
+      { apply iff.pi_iff_pi, intro a, esimp, apply is_hprop_iff_is_contr, reflexivity}},
+    { intro A, esimp [Iterated_loop_space],
+      transitivity _, apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, constructor,
+      apply iff.pi_iff_pi, intro a, transitivity _, apply IH,
+      transitivity _, apply iff.pi_iff_pi, intro p,
+      rewrite [iterated_loop_space_loop_irrel n p], apply iff.refl, esimp,
+      apply iff.imp_iff, reflexivity}
   end
 
   theorem is_trunc_iff_is_contr_loop (n : ℕ) (A : Type)