lemmas about dependent loop space

GroundZero/HITs/Sphere.lean

@@ -5,6 +5,7 @@ open GroundZero.HITs.Interval
 open GroundZero.Types.Equiv
 open GroundZero.Structures
 open GroundZero.Types.Id
+open GroundZero.Theorems
 open GroundZero.Types
 
 namespace GroundZero
@@ -16,7 +17,7 @@ namespace HigherSphere
   open GroundZero.HITs.Suspension (north south merid σ suspΩ)
   open GroundZero.Proto (idfun)
 
-  hott definition base : Π {n : ℕ}, S n
+  hott definition base : Π {n : ℕ}, Sⁿ
   | Nat.zero   => false
   | Nat.succ _ => north
 
@@ -208,22 +209,23 @@ namespace HigherSphere
     rec Sⁿ⁺¹ a n α ∘ rec Sⁿ⁺¹ b n β ~ rec Sⁿ⁺¹ (rec Sⁿ⁺¹ a n α b) n (mult α β) :=
   by apply recComMapΩ
 
-  hott definition irot {n : ℕ} : Π x, Ωⁿ⁺¹(∥Sⁿ⁺¹∥ₙ₊₁, x) :=
+  hott definition rotε {n : ℕ} : Π x, Ωⁿ⁺¹(∥Sⁿ⁺¹∥ₙ₊₁, x) :=
   Trunc.ind
     (ind n _ (apΩ Trunc.elem (surf n))
       (match n with
-      | Nat.zero   => Equiv.transportOverHmtpy _ _ _ _ ⬝ ap (· ⬝ _ ⬝ _) (Id.mapInv _ _) ⬝ ap (· ⬝ apΩ Trunc.elem (surf Nat.zero)) (Id.invComp _)
-      | Nat.succ n => inOverΩ _ _ (propRespectsEquiv (Equiv.altDefOverΩ _ _).symm
-                                                     (zeroEqvSet.forward (levelOverΩ _ (λ _, zeroTypeLoop (Trunc.uniq _) _) _) _ _) _ _)))
+      | Nat.zero   => Equiv.transportOverHmtpy _ _ _ _ ⬝ ap (· ⬝ _ ⬝ _) (Id.mapInv _ _) ⬝
+                      ap (· ⬝ apΩ Trunc.elem (surf Nat.zero)) (Id.invComp _)
+      | Nat.succ n => loopOverHSet (λ _, hsetLoop (Trunc.uniq _) _)))
     (λ _, levelStableΩ _ (Trunc.uniq _))
 
   hott definition code {n : ℕ} : Sⁿ⁺² → Type :=
   rec Type ∥Sⁿ⁺¹∥ₙ₊₁ (n + 1)
-    (conjugateΩ (uaidp ∥Sⁿ⁺¹∥ₙ₊₁) (apΩ ua (sigmaProdΩ (funextΩ idfun irot)
-      (inOverΩ _ _ (minusOneEqvProp.forward (levelOverΩ −1 (λ _, minusOneEqvProp.left (Theorems.Equiv.biinvProp _)) _) _ _)))))
+    (conjugateΩ (uaidp ∥Sⁿ⁺¹∥ₙ₊₁)
+                (apΩ ua (sigmaProdΩ (funextΩ idfun rotε)
+                                    (loopOverProp (λ _, Equiv.biinvProp _)))))
 
   hott lemma codeHLevel {n : ℕ} : Π (x : Sⁿ⁺²), is-(n + 1)-type (code x) :=
-  ind _ _ (Trunc.uniq _) (inOverΩ _ _ (minusOneEqvProp.forward (levelOverΩ −1 (λ _, minusOneEqvProp.left (ntypeIsProp _)) _) _ _))
+  ind _ _ (Trunc.uniq _) (loopOverProp (λ _, ntypeIsProp _))
 
   hott definition encode {n : ℕ} : Π (x : Sⁿ⁺²), ∥base = x∥ₙ₊₁ → code x :=
   λ x, Trunc.rec (λ ε, transport code ε |base|ₙ₊₁) (codeHLevel x)

GroundZero/HITs/Trunc.lean

@@ -4,6 +4,7 @@ open GroundZero.HITs.Interval (happly funext)
 open GroundZero.Structures.hlevel (succ)
 open GroundZero.Types.Id (ap)
 open GroundZero.Proto (idfun)
+open GroundZero.Types.Equiv
 open GroundZero.Structures
 open GroundZero.Types
 
@@ -118,6 +119,10 @@ namespace Trunc
   hott theorem respectsEquiv {A : Type u} {B : Type v} {n : ℕ₋₂} (φ : A ≃ B) : ∥A∥ₙ ≃ ∥B∥ₙ :=
   ⟨ap φ.forward, (⟨ap φ.left,  (apCom _ _).trans ((happly (Id.ap ap (funext φ.leftForward))).trans  idmap)⟩,
                   ⟨ap φ.right, (apCom _ _).trans ((happly (Id.ap ap (funext φ.forwardRight))).trans idmap)⟩)⟩
+
+  hott lemma transportOverTrunc {A : Type u} {n : ℕ₋₂} {B : A → Type v} {a b : A}
+    (p : a = b) (u : ∥B a∥ₙ) : transport (∥B ·∥ₙ) p u = Trunc.ap (transport B p) u :=
+  begin induction p; symmetry; apply Trunc.idmap end
 end Trunc
 
 end GroundZero.HITs

GroundZero/Structures.lean

@@ -1145,6 +1145,41 @@ namespace Types.Id
 
   hott corollary hsetLoop {A : Type u} {n : ℕ} (H : is-n-type A) : Π x, hset Ωⁿ(A, x) :=
   λ x, zeroEqvSet (zeroTypeLoop H x)
+
+  hott definition loopOverProp {A : Type u} {B : A → Type v} (H : Π x, prop (B x))
+    {n : ℕ} {a : A} {b : B a} {α : Ωⁿ⁺¹(A, a)} : Ωⁿ⁺¹(B, b, α) :=
+  inOverΩ _ _ (minusOneEqvProp.forward (levelOverΩ −1 (λ _, minusOneEqvProp.left (H _)) _) _ _)
+
+  hott definition loopOverHSet {A : Type u} {B : A → Type v} (H : Π x, hset (B x))
+    {n : ℕ} {a : A} {b : B a} {α : Ωⁿ⁺²(A, a)} : Ωⁿ⁺²(B, b, α) :=
+  inOverΩ _ _ (propRespectsEquiv (Equiv.altDefOverΩ _ _).symm
+    (zeroEqvSet.forward (levelOverΩ 0 (λ _, zeroEqvSet.left (H _)) _) _ _) _ _)
+
+  hott definition loopPropNType {A : Type u} : Π {n : ℕ} (H : is-n-type A) (a : A), prop Ωⁿ⁺¹(A, a)
+  | Nat.zero,   H, _ => zeroEqvSet.forward H _ _
+  | Nat.succ n, H, a => @loopPropNType (a = a) n (H a a) (idp a)
+
+  hott definition loopOverPropNType {A : Type u} {B : A → Type v} :
+    Π {n : ℕ} (H : Π x, is-n-type (B x)) {a : A} {b : B a} {α : Ωⁿ⁺¹(A, a)}, prop Ωⁿ⁺¹(B, b, α)
+  | Nat.zero,   H, _, _ => zeroEqvSet.forward (H _) _ _
+  | Nat.succ n, H, a, _ => @loopOverPropNType (a = a) _ n (λ _, H _ _ _) _ _ _
+
+  hott definition loopOverNType {A : Type u} {B : A → Type v} {n : ℕ} (H : Π x, is-n-type (B x))
+    {a : A} {b : B a} {α : Ωⁿ⁺²(A, a)} : Ωⁿ⁺²(B, b, α) :=
+  inOverΩ _ _ (loopOverPropNType H _ _)
+
+  hott definition ofApEqΩ {A : Type u} (B : A → Type v) {a : A} {b : B a} :
+    Π {n : ℕ} {α : Ωⁿ⁺¹(A, a)}, apΩ (transport B · b) α = idΩ b n → Ωⁿ⁺¹(B, b, α)
+  | Nat.zero,   α, β => β
+  | Nat.succ n, α, β =>
+  begin
+    apply @ofApEqΩ (a = a) (λ p, b =[B, p] b) (idp a) (idp b) n α;
+    apply Id.trans; apply apWithHomotopyΩ; intro;
+    transitivity; apply transportOverContrMap;
+    transitivity; apply rid; apply mapInv;
+    transitivity; apply comApΩ Id.inv;
+    transitivity; apply ap (apΩ _); exact β; apply apIdΩ;
+  end
 end Types.Id
 
 end GroundZero

GroundZero/Types/Equiv.lean

@@ -818,6 +818,10 @@ namespace Equiv
   | Nat.zero,   p => Id.invComp p
   | Nat.succ n, α => @revlΩ (a = a) (idp a) n α
 
+  hott lemma idrevΩ {A : Type u} {a : A} : Π {n : ℕ}, revΩ (idΩ a (n + 1)) = idΩ a (n + 1)
+  | Nat.zero   => idp (idp a)
+  | Nat.succ n => @idrevΩ (a = a) (idp a) n
+
   hott theorem involΩ {A : Type u} {a : A} : Π {n : ℕ} (α : Ωⁿ⁺¹(A, a)), revΩ (revΩ α) = α
   | Nat.zero,   p => Id.invInv p
   | Nat.succ n, α => @involΩ (a = a) (idp a) n α