diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean
index 305cedd..e7d0052 100644
--- a/GroundZero/HITs/Circle.lean
+++ b/GroundZero/HITs/Circle.lean
@@ -661,6 +661,18 @@ namespace Circle
     { intro φ; symmetry; apply Theorems.funext; apply mapExt }
   end
 
+  hott theorem loopCircle {A : Type u} (a : A) : Map⁎ ⟨S¹, base⟩ ⟨A, a⟩ ≃ (a = a) :=
+  begin
+    fapply Sigma.mk; intro φ; exact transport (λ x, x = x) φ.2 (ap φ.1 loop); apply Qinv.toBiinv;
+    fapply Sigma.mk; intro p; existsi rec a p; reflexivity; apply Prod.mk;
+    { intro; apply recβrule₂ };
+    { intro ⟨φ, (H : φ base = a)⟩; induction H using J₁;
+      fapply Sigma.prod; symmetry; apply Theorems.funext; apply mapExt;
+      transitivity; apply transportOverContrMap; transitivity; apply Id.rid;
+      transitivity; apply ap (ap _); apply Id.invInv; transitivity; apply Theorems.mapToHapply;
+      transitivity; apply happly; apply Theorems.happlyFunext; reflexivity }
+  end
+
   noncomputable hott lemma recBaseInj {x : S¹} (p q : x = x) (ε : rec x p = rec x q) : p = q :=
   begin
     have θ := ap (subst ε) (recβrule₂ x p)⁻¹ ⬝ apd (λ f, ap f loop) ε ⬝ recβrule₂ x q;
@@ -1378,16 +1390,19 @@ namespace Torus
 end Torus
 
 namespace HigherSphere
-  open GroundZero.HITs.Suspension (north merid σ)
+  open GroundZero.HITs.Suspension (north merid σ suspΩ)
   open GroundZero.Proto (idfun)
 
   hott def base : Π {n : ℕ}, S n
   | Nat.zero   => false
   | Nat.succ _ => north
 
-  hott def surf : Π (n : ℕ), Ωⁿ⁺¹(Sⁿ⁺¹)
-  | Nat.zero   => Circle.loop
-  | Nat.succ n => conjugateΩ (compInv _) (apΩ σ (surf n))
+  hott def diag : Π (n : ℕ), Ω¹(S¹) → Ωⁿ⁺¹(Sⁿ⁺¹)
+  | Nat.zero   => idfun
+  | Nat.succ n => suspΩ ∘ diag n
+
+  hott def surf (n : ℕ) : Ωⁿ⁺¹(Sⁿ⁺¹) :=
+  diag n Circle.loop
 
   hott def rec (B : Type u) (b : B) : Π (n : ℕ), Ωⁿ⁺¹(B, b) → Sⁿ⁺¹ → B
   | Nat.zero   => Circle.rec b
@@ -1482,6 +1497,12 @@ namespace HigherSphere
     apply Suspension.σRevComMerid
   end
 
+  noncomputable hott corollary constRecΩ (n : ℕ) : rec Sⁿ⁺¹ base n (idΩ base (n + 1)) ~ (λ _, base) :=
+  begin
+    transitivity; apply Homotopy.Id; apply ap (rec Sⁿ⁺¹ base n); symmetry;
+    apply constmapΩ (n + 1) (surf n); apply mapExtΩ n (λ _, base)
+  end
+
   -- Direct proof of universal property of Sⁿ⁺¹.
   hott theorem mapLoopEqvΩ {B : Type u} : Π (n : ℕ), (Sⁿ⁺¹ → B) ≃ (Σ (x : B), Ωⁿ⁺¹(B, x))
   | Nat.zero   => Circle.mapLoopEqv
@@ -1493,6 +1514,21 @@ namespace HigherSphere
     { intro φ; apply Theorems.funext; apply mapExtΩ }
   end
 
+  hott theorem loopSphere {A : Type u} (a : A) : Π (n : ℕ), Map⁎ ⟨Sⁿ⁺¹, base⟩ ⟨A, a⟩ ≃ Ωⁿ⁺¹(A, a)
+  | Nat.zero   => Circle.loopCircle a
+  | Nat.succ n =>
+  begin
+    fapply Sigma.mk; intro φ; exact conjugateΩ φ.2 (apΩ φ.1 (surf (n + 1))); apply Qinv.toBiinv;
+    fapply Sigma.mk; intro ε; existsi rec A a (n + 1) ε; reflexivity; apply Prod.mk;
+    { intro; apply recβrule₂ };
+    { intro ⟨φ, (H : φ base = a)⟩; induction H using J₁;
+      fapply Sigma.prod; apply Theorems.funext; apply mapExtΩ;
+      transitivity; apply transportOverContrMap; transitivity; apply Id.rid;
+      transitivity; apply mapInv; transitivity; apply ap;
+      transitivity; apply Theorems.mapToHapply; apply happly;
+      apply Theorems.happlyFunext; reflexivity }
+  end
+
   hott def indBias (n : ℕ) (B : Sⁿ⁺¹ → Type u) (b : B base) (ε : Ωⁿ⁺¹(B, b, surf n)) :=
   rec (Σ x, B x) ⟨base, b⟩ n (sigmaProdΩ (surf n) ε)
 
@@ -1536,6 +1572,13 @@ namespace HigherSphere
   hott theorem indβrule₁ : Π (n : ℕ) (B : Sⁿ⁺¹ → Type u) (b : B base) (α : Ωⁿ⁺¹(B, b, surf n)), ind n B b α base = b
   | Nat.zero,   _, _, _ => idp _
   | Nat.succ _, _, _, _ => idp _
+
+  hott def mult {n : ℕ} {a b : Sⁿ⁺¹} (α : Ωⁿ⁺¹(Sⁿ⁺¹, a)) (β : Ωⁿ⁺¹(Sⁿ⁺¹, b)) : Ωⁿ⁺¹(Sⁿ⁺¹, rec Sⁿ⁺¹ a n α b) :=
+  apΩ (rec Sⁿ⁺¹ a n α) β
+
+  hott corollary recCompΩ {n : ℕ} {a b : Sⁿ⁺¹} (α : Ωⁿ⁺¹(Sⁿ⁺¹, a)) (β : Ωⁿ⁺¹(Sⁿ⁺¹, b)) :
+    rec Sⁿ⁺¹ a n α ∘ rec Sⁿ⁺¹ b n β ~ rec Sⁿ⁺¹ (rec Sⁿ⁺¹ a n α b) n (mult α β) :=
+  by apply recComMapΩ
 end HigherSphere
 
 namespace Sphere
diff --git a/GroundZero/HITs/Suspension.lean b/GroundZero/HITs/Suspension.lean
index badbca5..a31740c 100644
--- a/GroundZero/HITs/Suspension.lean
+++ b/GroundZero/HITs/Suspension.lean
@@ -1,8 +1,8 @@
 import GroundZero.HITs.Pushout
 import GroundZero.Types.Unit
 
-open GroundZero.Types.Id (ap isPointed pointOf)
 open GroundZero.Types.Equiv
+open GroundZero.Types.Id
 open GroundZero.Types
 
 /-
@@ -56,6 +56,22 @@ namespace Suspension
 
   hott lemma σRevComMerid {A : Type u} [isPointed A] (x : A) : (σ x)⁻¹ ⬝ merid x = merid (pointOf A) :=
   begin apply rewriteComp; symmetry; apply σComMerid end
+
+  section
+    variable {A : Type u} [isPointed A] {n : ℕ}
+
+    hott def suspΩ : Ωⁿ(A) → Ωⁿ⁺¹(∑ A) :=
+    λ ε, conjugateΩ (compInv (merid (pointOf A))) (apΩ σ ε)
+
+    hott lemma suspIdΩ : suspΩ (idΩ (pointOf A) n) = idΩ north (n + 1) :=
+    begin transitivity; apply ap (conjugateΩ _); apply apIdΩ; apply conjugateIdΩ end
+
+    hott lemma suspRevΩ (α : Ωⁿ⁺¹(A)) : suspΩ (revΩ α) = revΩ (suspΩ α) :=
+    begin transitivity; apply ap (conjugateΩ _); apply apRevΩ; apply conjugateRevΩ end
+
+    hott lemma suspMultΩ (α β : Ωⁿ⁺¹(A)) : suspΩ (comΩ α β) = comΩ (suspΩ α) (suspΩ β) :=
+    begin transitivity; apply ap (conjugateΩ _); apply apFunctorialityΩ; apply conjugateComΩ end
+  end
 end Suspension
 
 end HITs
diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean
index 994f0ba..d81c35f 100644
--- a/GroundZero/Structures.lean
+++ b/GroundZero/Structures.lean
@@ -925,6 +925,10 @@ namespace Types.Id
   | Nat.zero,   _ => idp _
   | Nat.succ _, _ => apWithHomotopyΩ idmap _ _ ⬝ idmapΩ _ _
 
+  hott lemma constmapΩ {A : Type u} {B : Type v} {a : A} {b : B} : Π (n : ℕ) (α : Ωⁿ(A, a)), apΩ (λ _, b) α = idΩ b n
+  | Nat.zero,   _ => idp _
+  | Nat.succ n, _ => apWithHomotopyΩ constmap _ _ ⬝ constmapΩ _ _
+
   hott lemma conjugateSuccΩ {A : Type u} {a b : A} (p : a = b) (n : ℕ) (α : Ωⁿ⁺¹(A, a)) :
     α^p = conjugateΩ (apd idp p) (apΩ (transport (λ x, x = x) p) α) :=
   begin induction p; symmetry; apply idmapΩ end
diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean
index ae106d3..212d0a1 100644
--- a/GroundZero/Types/Equiv.lean
+++ b/GroundZero/Types/Equiv.lean
@@ -907,6 +907,51 @@ namespace Equiv
     abbrev outOverΩ : Ωⁿ⁺¹(B, b, α) → Ω¹(λ β, Ωⁿ(B, b, β), idOverΩ b n, outΩ n α) := (altDefOverΩ n α).forward
     abbrev inOverΩ  : Ω¹(λ β, Ωⁿ(B, b, β), idOverΩ b n, outΩ n α) → Ωⁿ⁺¹(B, b, α) := (altDefOverΩ n α).left
   end
+
+  hott theorem apIdΩ {A : Type u} {B : Type v} (f : A → B) {a : A} : Π {n : ℕ}, apΩ f (idΩ a n) = idΩ (f a) n
+  | Nat.zero   => idp (f a)
+  | Nat.succ n => @apIdΩ (a = a) (f a = f a) (ap f) (idp a) n
+
+  hott theorem apRevΩ {A : Type u} {B : Type v} (f : A → B) {a : A} :
+    Π {n : ℕ} (α : Ωⁿ⁺¹(A, a)), apΩ f (revΩ α) = revΩ (apΩ f α)
+  | Nat.zero,   p => Id.mapInv f p
+  | Nat.succ n, α => @apRevΩ (a = a) (f a = f a) (ap f) (idp a) n α
+
+  hott theorem apFunctorialityΩ {A : Type u} {B : Type v} (f : A → B) {a : A} :
+    Π {n : ℕ} (α β : Ωⁿ⁺¹(A, a)), apΩ f (comΩ α β) = comΩ (apΩ f α) (apΩ f β)
+  | Nat.zero,   _, _ => mapFunctoriality f
+  | Nat.succ n, α, β => @apFunctorialityΩ (a = a) (f a = f a) (ap f) (idp a) n α β
+
+  hott corollary apFunctorialityΩ₃ {A : Type u} {B : Type v} (f : A → B) {a : A} {n : ℕ}
+    (α β γ : Ωⁿ⁺¹(A, a)) : apΩ f (comΩ (comΩ α β) γ) = comΩ (comΩ (apΩ f α) (apΩ f β)) (apΩ f γ) :=
+  begin transitivity; apply apFunctorialityΩ; apply ap (comΩ · _); apply apFunctorialityΩ end
+
+  section
+    variable {A : Type u} {a b : A} (p : a = b) {n : ℕ}
+
+    hott lemma conjugateIdΩ : idΩ a n ^ p = idΩ b n :=
+    begin induction p; reflexivity end
+
+    hott lemma conjugateRevΩ (α : Ωⁿ⁺¹(A, a)) : revΩ α ^ p = revΩ (α ^ p) :=
+    begin induction p; reflexivity end
+
+    hott lemma conjugateComΩ (α β : Ωⁿ⁺¹(A, a)) : comΩ α β ^ p = comΩ (α ^ p) (β ^ p) :=
+    begin induction p; reflexivity end
+  end
+
+  hott lemma transportOverHmtpyΩ {A : Type u} {B : Type v} (f : A → B) {a b : A} {n : ℕ}
+    (p : a = b) (α : Ωⁿ(B, f a)) : transport (λ x, Ωⁿ(B, f x)) p α = conjugateΩ (ap f p) α :=
+  by apply transportComp (λ y, Ωⁿ(B, y)) f
+
+  hott theorem bimapCharacterizationΩ₁ {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) {a : A} {b : B} :
+    Π {n : ℕ} (α : Ωⁿ⁺¹(A, a)) (β : Ωⁿ⁺¹(B, b)), bimapΩ f α β = comΩ (apΩ (f · b) α) (apΩ (f a) β)
+  | Nat.zero,   _, _ => bimapCharacterization f _ _
+  | Nat.succ n, α, β => @bimapCharacterizationΩ₁ (a = a) (b = b) (f a b = f a b) (bimap f) (idp a) (idp b) n α β
+
+  hott theorem bimapCharacterizationΩ₂ {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) {a : A} {b : B} :
+    Π {n : ℕ} (α : Ωⁿ⁺¹(A, a)) (β : Ωⁿ⁺¹(B, b)), bimapΩ f α β = comΩ (apΩ (f a) β) (apΩ (f · b) α)
+  | Nat.zero,   _, _ => bimapCharacterization' f _ _
+  | Nat.succ n, α, β => @bimapCharacterizationΩ₂ (a = a) (b = b) (f a b = f a b) (bimap f) (idp a) (idp b) n α β
 end Equiv
 
 end GroundZero.Types