diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean index b8d2f2e..f65c18f 100644 --- a/GroundZero/HITs/Circle.lean +++ b/GroundZero/HITs/Circle.lean @@ -338,10 +338,10 @@ namespace Circle change _ = idp _ ⬝ loop; apply ap (· ⬝ loop); apply Id.invComp end - def μₑ : S¹ → S¹ ≃ S¹ := + hott def μₑ : S¹ → S¹ ≃ S¹ := Circle.rec (ideqv S¹) (Sigma.prod (Theorems.funext rot) (Theorems.Equiv.biinvProp _ _ _)) - def μ (x : S¹) : S¹ → S¹ := (μₑ x).forward + hott def μ (x : S¹) : S¹ → S¹ := (μₑ x).forward hott def μLoop : ap μ loop = Theorems.funext rot := begin @@ -1392,239 +1392,6 @@ namespace Torus Φ Circle.loop Circle.loop end Torus -namespace HigherSphere - 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 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 - | Nat.succ n => λ ε, Suspension.rec b b (rec (b = b) (idp b) n ε) - - hott theorem recβrule₁ {B : Type u} (b : B) : Π {n : ℕ} (α : Ωⁿ⁺¹(B, b)), rec B b n α base = b - | Nat.zero, _ => idp _ - | Nat.succ _, _ => idp _ - - hott lemma σComApRec {B : Type u} (b : B) (n : ℕ) (ε : Ωⁿ⁺²(B, b)) : - ap (rec B b (n + 1) ε) ∘ σ ~ rec (b = b) (idp b) n ε := - begin - intro x; transitivity; apply mapFunctoriality; - transitivity; apply bimap; apply Suspension.recβrule; - transitivity; apply Id.mapInv; apply ap; - apply Suspension.recβrule; transitivity; apply ap (_ ⬝ ·); - apply ap; apply recβrule₁; apply Id.rid - end - - hott theorem recβrule₂ {B : Type u} (b : B) : Π (n : ℕ) (α : Ωⁿ⁺¹(B, b)), - conjugateΩ (recβrule₁ b α) (apΩ (rec B b n α) (surf n)) = α - | Nat.zero, _ => Circle.recβrule₂ _ _ - | Nat.succ n, _ => - begin - show apΩ (ap _) (conjugateΩ _ _) = _; - transitivity; apply apConjugateΩ; transitivity; apply ap (conjugateΩ _); - transitivity; symmetry; apply comApΩ _ σ; apply apWithHomotopyΩ; - apply σComApRec; transitivity; symmetry; apply conjugateTransΩ; - transitivity; apply ap (conjugateΩ _); symmetry; apply conjugateRevRightΩ; - apply recβrule₁; transitivity; symmetry; apply conjugateTransΩ; - transitivity; apply ap (conjugateΩ _); apply recβrule₂ _ n; apply abelianΩ - end - - hott lemma recConjugateΩ {A : Type u} {a b : A} (p : a = b) - (n : ℕ) (α : Ωⁿ⁺¹(A, a)) : rec A b n (α^p) ~ rec A a n α := - begin induction p; reflexivity end - - hott theorem recComMapΩ {A : Type u} {B : Type v} (φ : A → B) (a : A) : - Π (n : ℕ) (α : Ωⁿ⁺¹(A, a)), φ ∘ rec A a n α ~ rec B (φ a) n (apΩ φ α) - | Nat.zero, _ => Circle.recComMap _ _ _ - | Nat.succ n, α => - begin - fapply Suspension.ind; reflexivity; reflexivity; intro x; - apply Id.trans; apply Equiv.transportOverHmtpy; - transitivity; apply ap (· ⬝ _); apply Id.rid; - transitivity; apply bimap; - { transitivity; apply mapInv; apply ap; - transitivity; apply mapOverComp; - transitivity; apply ap (ap φ); apply Suspension.recβrule; - apply recComMapΩ (ap φ) _ n }; - { apply Suspension.recβrule }; - apply invComp - end - - hott theorem idfunRecΩ : Π (n : ℕ), rec Sⁿ⁺¹ base n (surf n) ~ idfun - | Nat.zero => Circle.map.nontrivialHmtpy - | Nat.succ n => - begin - fapply Suspension.ind; reflexivity; apply merid base; intro x; - apply Id.trans; apply Equiv.transportOverHmtpy; - transitivity; apply ap (· ⬝ _); apply Id.rid; - transitivity; apply bimap; - { transitivity; apply mapInv; apply ap; - transitivity; apply Suspension.recβrule; - transitivity; apply @recConjugateΩ (base = base); - transitivity; symmetry; apply recComMapΩ σ; - apply ap σ; apply idfunRecΩ n }; - { apply idmap }; - apply Suspension.σRevComMerid - end - - hott lemma σRecΩ (n : ℕ) : rec (@Id Sⁿ⁺² base base) (idp base) n (surf (n + 1)) ~ σ := - begin - transitivity; apply recConjugateΩ; - transitivity; symmetry; apply recComMapΩ σ; - apply Homotopy.rwhs; apply idfunRecΩ - end - - hott theorem mapExtΩ {B : Type u} : Π (n : ℕ) (φ : Sⁿ⁺¹ → B), rec B (φ base) n (apΩ φ (surf n)) ~ φ - | Nat.zero => λ _ _, (Circle.mapExt _ _)⁻¹ - | Nat.succ n => - begin - intro φ; fapply Suspension.ind; reflexivity; apply ap φ (merid base); - intro x; apply Id.trans; apply Equiv.transportOverHmtpy; - transitivity; apply ap (· ⬝ _); transitivity; apply Id.rid; - transitivity; apply mapInv; transitivity; apply ap; - transitivity; apply Suspension.recβrule; dsimp [apΩ]; - symmetry; apply recComMapΩ (ap φ) (idp base); - symmetry; apply mapInv φ; transitivity; symmetry; - apply mapFunctoriality φ; apply ap (ap φ); - transitivity; apply ap (·⁻¹ ⬝ _); apply σRecΩ; - apply Suspension.σRevComMerid - end - - 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 - | Nat.succ n => - begin - fapply Sigma.mk; intro φ; exact ⟨φ base, apΩ φ (surf (n + 1))⟩; apply Qinv.toBiinv; - fapply Sigma.mk; intro w; exact rec B w.1 (n + 1) w.2; apply Prod.mk; - { intro; fapply Sigma.prod; reflexivity; apply recβrule₂ }; - { 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) ε) - - hott example (n : ℕ) (B : Sⁿ⁺¹ → Type u) (b : B base) - (ε : Ωⁿ⁺¹(B, b, surf n)) (x : Sⁿ⁺¹) : (indBias n B b ε x).1 = x := - begin - transitivity; apply recComMapΩ; - transitivity; apply ap (rec _ _ _ · _); - apply apFstProdΩ; apply idfunRecΩ - end - - -- this (longer) proof computes better than the previous one - hott lemma indBiasPath : Π (n : ℕ) (B : Sⁿ⁺¹ → Type u) - (b : B base) (ε : Ωⁿ⁺¹(B, b, surf n)), Π x, (indBias n B b ε x).1 = x - | Nat.zero => - begin - intro B b ε; fapply Circle.ind; reflexivity; apply Id.trans; - transitivity; apply transportOverInvolution; apply ap (· ⬝ _); - transitivity; apply Id.rid; transitivity; apply mapInv; apply ap; - transitivity; apply mapOverComp; - transitivity; apply ap (ap Sigma.fst); - dsimp [indBias]; apply Circle.recβrule₂; - apply Sigma.mapFstOverProd; apply invComp - end - | Nat.succ n => - begin - intro B b ε; fapply Suspension.ind; reflexivity; exact merid base; - intro x; apply Id.trans; apply transportOverInvolution; - transitivity; apply ap (· ⬝ _); transitivity; apply Id.rid; - transitivity; apply mapInv; apply ap; - transitivity; apply mapOverComp; - transitivity; apply ap (ap Sigma.fst); dsimp [indBias]; apply Suspension.recβrule; - transitivity; apply recComMapΩ; transitivity; apply ap (rec _ _ _ · _); - apply @apFstProdΩ Sⁿ⁺² B ⟨base, b⟩ (n + 2) (surf (n + 1)) ε; - apply σRecΩ; apply Suspension.σRevComMerid - end - - hott def ind (n : ℕ) (B : Sⁿ⁺¹ → Type u) (b : B base) (ε : Ωⁿ⁺¹(B, b, surf n)) : Π x, B x := - λ x, transport B (indBiasPath n B b ε x) (indBias n B b ε x).2 - - 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 - open GroundZero.HITs.Suspension (σ) - - hott def base : S² := HigherSphere.base - - hott def surf : idp base = idp base := - HigherSphere.surf 1 - - section - variable {B : Type u} (b : B) (ε : idp b = idp b) - - hott def rec : S² → B := HigherSphere.rec B b 1 ε - - hott corollary recβrule₁ : rec b ε base = b := idp b - - hott corollary recβrule₂ : ap² (rec b ε) surf = ε := - HigherSphere.recβrule₂ b 1 ε - end - - hott def cup : S¹ → S¹ → S² := - Circle.rec (λ _, base) (Theorems.funext σ) -end Sphere - -namespace Glome - hott def base : S³ := HigherSphere.base - - hott def surf : idp (idp base) = idp (idp base) := - HigherSphere.surf 2 - - section - variable {B : Type u} (b : B) (ε : idp (idp b) = idp (idp b)) - - hott def rec : S³ → B := HigherSphere.rec B b 2 ε - - hott corollary recβrule₁ : rec b ε base = b := idp b - - hott corollary recβrule₂ : ap³ (rec b ε) surf = ε := - HigherSphere.recβrule₂ b 2 ε - end -end Glome - end HITs namespace Types.Integer diff --git a/GroundZero/HITs/Sphere.lean b/GroundZero/HITs/Sphere.lean new file mode 100644 index 0000000..c7ad1ea --- /dev/null +++ b/GroundZero/HITs/Sphere.lean @@ -0,0 +1,248 @@ +import GroundZero.HITs.Circle + +open GroundZero.HITs.Interval +open GroundZero.Types.Equiv +open GroundZero.Structures +open GroundZero.Types.Id +open GroundZero.Types + +namespace GroundZero +namespace HITs + +universe u v w + +namespace HigherSphere + 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 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 + | Nat.succ n => λ ε, Suspension.rec b b (rec (b = b) (idp b) n ε) + + hott theorem recβrule₁ {B : Type u} (b : B) : Π {n : ℕ} (α : Ωⁿ⁺¹(B, b)), rec B b n α base = b + | Nat.zero, _ => idp _ + | Nat.succ _, _ => idp _ + + hott lemma σComApRec {B : Type u} (b : B) (n : ℕ) (ε : Ωⁿ⁺²(B, b)) : + ap (rec B b (n + 1) ε) ∘ σ ~ rec (b = b) (idp b) n ε := + begin + intro x; transitivity; apply mapFunctoriality; + transitivity; apply bimap; apply Suspension.recβrule; + transitivity; apply Id.mapInv; apply ap; + apply Suspension.recβrule; transitivity; apply ap (_ ⬝ ·); + apply ap; apply recβrule₁; apply Id.rid + end + + hott theorem recβrule₂ {B : Type u} (b : B) : Π (n : ℕ) (α : Ωⁿ⁺¹(B, b)), + conjugateΩ (recβrule₁ b α) (apΩ (rec B b n α) (surf n)) = α + | Nat.zero, _ => Circle.recβrule₂ _ _ + | Nat.succ n, _ => + begin + show apΩ (ap _) (conjugateΩ _ _) = _; + transitivity; apply apConjugateΩ; transitivity; apply ap (conjugateΩ _); + transitivity; symmetry; apply comApΩ _ σ; apply apWithHomotopyΩ; + apply σComApRec; transitivity; symmetry; apply conjugateTransΩ; + transitivity; apply ap (conjugateΩ _); symmetry; apply conjugateRevRightΩ; + apply recβrule₁; transitivity; symmetry; apply conjugateTransΩ; + transitivity; apply ap (conjugateΩ _); apply recβrule₂ _ n; apply abelianΩ + end + + hott lemma recConjugateΩ {A : Type u} {a b : A} (p : a = b) + (n : ℕ) (α : Ωⁿ⁺¹(A, a)) : rec A b n (α^p) ~ rec A a n α := + begin induction p; reflexivity end + + hott theorem recComMapΩ {A : Type u} {B : Type v} (φ : A → B) (a : A) : + Π (n : ℕ) (α : Ωⁿ⁺¹(A, a)), φ ∘ rec A a n α ~ rec B (φ a) n (apΩ φ α) + | Nat.zero, _ => Circle.recComMap _ _ _ + | Nat.succ n, α => + begin + fapply Suspension.ind; reflexivity; reflexivity; intro x; + apply Id.trans; apply Equiv.transportOverHmtpy; + transitivity; apply ap (· ⬝ _); apply Id.rid; + transitivity; apply bimap; + { transitivity; apply mapInv; apply ap; + transitivity; apply mapOverComp; + transitivity; apply ap (ap φ); apply Suspension.recβrule; + apply recComMapΩ (ap φ) _ n }; + { apply Suspension.recβrule }; + apply invComp + end + + hott theorem idfunRecΩ : Π (n : ℕ), rec Sⁿ⁺¹ base n (surf n) ~ idfun + | Nat.zero => Circle.map.nontrivialHmtpy + | Nat.succ n => + begin + fapply Suspension.ind; reflexivity; apply merid base; intro x; + apply Id.trans; apply Equiv.transportOverHmtpy; + transitivity; apply ap (· ⬝ _); apply Id.rid; + transitivity; apply bimap; + { transitivity; apply mapInv; apply ap; + transitivity; apply Suspension.recβrule; + transitivity; apply @recConjugateΩ (base = base); + transitivity; symmetry; apply recComMapΩ σ; + apply ap σ; apply idfunRecΩ n }; + { apply idmap }; + apply Suspension.σRevComMerid + end + + hott lemma σRecΩ (n : ℕ) : rec (@Id Sⁿ⁺² base base) (idp base) n (surf (n + 1)) ~ σ := + begin + transitivity; apply recConjugateΩ; + transitivity; symmetry; apply recComMapΩ σ; + apply Homotopy.rwhs; apply idfunRecΩ + end + + hott theorem mapExtΩ {B : Type u} : Π (n : ℕ) (φ : Sⁿ⁺¹ → B), rec B (φ base) n (apΩ φ (surf n)) ~ φ + | Nat.zero => λ _ _, (Circle.mapExt _ _)⁻¹ + | Nat.succ n => + begin + intro φ; fapply Suspension.ind; reflexivity; apply ap φ (merid base); + intro x; apply Id.trans; apply Equiv.transportOverHmtpy; + transitivity; apply ap (· ⬝ _); transitivity; apply Id.rid; + transitivity; apply mapInv; transitivity; apply ap; + transitivity; apply Suspension.recβrule; dsimp [apΩ]; + symmetry; apply recComMapΩ (ap φ) (idp base); + symmetry; apply mapInv φ; transitivity; symmetry; + apply mapFunctoriality φ; apply ap (ap φ); + transitivity; apply ap (·⁻¹ ⬝ _); apply σRecΩ; + apply Suspension.σRevComMerid + end + + 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 + | Nat.succ n => + begin + fapply Sigma.mk; intro φ; exact ⟨φ base, apΩ φ (surf (n + 1))⟩; apply Qinv.toBiinv; + fapply Sigma.mk; intro w; exact rec B w.1 (n + 1) w.2; apply Prod.mk; + { intro; fapply Sigma.prod; reflexivity; apply recβrule₂ }; + { 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) ε) + + hott example (n : ℕ) (B : Sⁿ⁺¹ → Type u) (b : B base) + (ε : Ωⁿ⁺¹(B, b, surf n)) (x : Sⁿ⁺¹) : (indBias n B b ε x).1 = x := + begin + transitivity; apply recComMapΩ; + transitivity; apply ap (rec _ _ _ · _); + apply apFstProdΩ; apply idfunRecΩ + end + + -- this (longer) proof computes better than the previous one + hott lemma indBiasPath : Π (n : ℕ) (B : Sⁿ⁺¹ → Type u) + (b : B base) (ε : Ωⁿ⁺¹(B, b, surf n)), Π x, (indBias n B b ε x).1 = x + | Nat.zero => + begin + intro B b ε; fapply Circle.ind; reflexivity; apply Id.trans; + transitivity; apply transportOverInvolution; apply ap (· ⬝ _); + transitivity; apply Id.rid; transitivity; apply mapInv; apply ap; + transitivity; apply mapOverComp; + transitivity; apply ap (ap Sigma.fst); + dsimp [indBias]; apply Circle.recβrule₂; + apply Sigma.mapFstOverProd; apply invComp + end + | Nat.succ n => + begin + intro B b ε; fapply Suspension.ind; reflexivity; exact merid base; + intro x; apply Id.trans; apply transportOverInvolution; + transitivity; apply ap (· ⬝ _); transitivity; apply Id.rid; + transitivity; apply mapInv; apply ap; + transitivity; apply mapOverComp; + transitivity; apply ap (ap Sigma.fst); dsimp [indBias]; apply Suspension.recβrule; + transitivity; apply recComMapΩ; transitivity; apply ap (rec _ _ _ · _); + apply @apFstProdΩ Sⁿ⁺² B ⟨base, b⟩ (n + 2) (surf (n + 1)) ε; + apply σRecΩ; apply Suspension.σRevComMerid + end + + hott def ind (n : ℕ) (B : Sⁿ⁺¹ → Type u) (b : B base) (ε : Ωⁿ⁺¹(B, b, surf n)) : Π x, B x := + λ x, transport B (indBiasPath n B b ε x) (indBias n B b ε x).2 + + 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 + open GroundZero.HITs.Suspension (σ) + + hott def base : S² := HigherSphere.base + + hott def surf : idp base = idp base := + HigherSphere.surf 1 + + section + variable {B : Type u} (b : B) (ε : idp b = idp b) + + hott def rec : S² → B := HigherSphere.rec B b 1 ε + + hott corollary recβrule₁ : rec b ε base = b := idp b + + hott corollary recβrule₂ : ap² (rec b ε) surf = ε := + HigherSphere.recβrule₂ b 1 ε + end + + hott def cup : S¹ → S¹ → S² := + Circle.rec (λ _, base) (Theorems.funext σ) +end Sphere + +namespace Glome + hott def base : S³ := HigherSphere.base + + hott def surf : idp (idp base) = idp (idp base) := + HigherSphere.surf 2 + + section + variable {B : Type u} (b : B) (ε : idp (idp b) = idp (idp b)) + + hott def rec : S³ → B := HigherSphere.rec B b 2 ε + + hott corollary recβrule₁ : rec b ε base = b := idp b + + hott corollary recβrule₂ : ap³ (rec b ε) surf = ε := + HigherSphere.recβrule₂ b 2 ε + end +end Glome + +end HITs +end GroundZero diff --git a/dependency-map.gv b/dependency-map.gv index 761fb1d..7d48f17 100644 --- a/dependency-map.gv +++ b/dependency-map.gv @@ -102,7 +102,8 @@ digraph dependency_map { "Algebra/Group/Z", "Theorems/Hopf", "HITs/Moebius", - "HITs/Reals" + "HITs/Reals", + "HITs/Sphere" } "HITs/Coequalizer" -> { "HITs/Flattening" } "HITs/Colimit" -> { "HITs/Merely", "Types/Nat" } @@ -139,6 +140,7 @@ digraph dependency_map { } "HITs/Reals" "HITs/Simplicial" + "HITs/Sphere" "HITs/Suspension" -> { "Algebra/EilenbergMacLane", "HITs/Circle", "HITs/Join" } "HITs/Topologization" "HITs/Trunc" -> { @@ -178,6 +180,7 @@ digraph dependency_map { subgraph Theorems { "Theorems/Classical" -> { "Algebra/Category", "Algebra/Orgraph" } + "Theorems/Connectedness" "Theorems/Fibration" -> { "Theorems/Hopf" } "Theorems/Functions" -> { "Modal/Etale", diff --git a/pictures/dependency-map.svg b/pictures/dependency-map.svg index db09269..218e608 100644 --- a/pictures/dependency-map.svg +++ b/pictures/dependency-map.svg @@ -4,1294 +4,1306 @@ - + dependency_map - + Proto - -Proto + +Proto Types/Id - -Types/Id + +Types/Id Proto->Types/Id - - + + Theorems/Ontological - -Theorems/Ontological + +Theorems/Ontological Proto->Theorems/Ontological - - + + Support - -Support + +Support Types/Id->Support - - + + Types/Equiv - -Types/Equiv + +Types/Equiv Support->Types/Equiv - - + + Types/Coproduct - -Types/Coproduct + +Types/Coproduct Types/Equiv->Types/Coproduct - - + + Types/HEq - -Types/HEq + +Types/HEq Types/Equiv->Types/HEq - - + + Modal/Infinitesimal - -Modal/Infinitesimal + +Modal/Infinitesimal Types/Equiv->Modal/Infinitesimal - - + + Types/Lost - -Types/Lost + +Types/Lost Types/Equiv->Types/Lost - - + + Types/Unit - -Types/Unit + +Types/Unit Types/Equiv->Types/Unit - - + + Types/Sigma - -Types/Sigma + +Types/Sigma Types/Equiv->Types/Sigma - - + + Structures - -Structures + +Structures HITs/Interval - -HITs/Interval + +HITs/Interval Structures->HITs/Interval - - + + HITs/Merely - -HITs/Merely + +HITs/Merely Structures->HITs/Merely - - + + Types/Nat - -Types/Nat + +Types/Nat Structures->Types/Nat - - + + Modal/Disc - -Modal/Disc + +Modal/Disc Structures->Modal/Disc - - + + - + Cubical/Cubes - -Cubical/Cubes + +Cubical/Cubes - + HITs/Interval->Cubical/Cubes - - + + - + Cubical/Path - -Cubical/Path + +Cubical/Path - + HITs/Interval->Cubical/Path - - + + - + Theorems/Equiv - -Theorems/Equiv + +Theorems/Equiv - + HITs/Interval->Theorems/Equiv - - + + - + Theorems/Fibration - -Theorems/Fibration + +Theorems/Fibration - + HITs/Interval->Theorems/Fibration - - + + - + HITs/Merely->Theorems/Equiv - - + + - + HITs/Simplicial - -HITs/Simplicial + +HITs/Simplicial - + HITs/Merely->HITs/Simplicial - - + + - + HITs/Trunc - -HITs/Trunc + +HITs/Trunc - + HITs/Merely->HITs/Trunc - - + + - + Theorems/Functions - -Theorems/Functions + +Theorems/Functions - + HITs/Merely->Theorems/Functions - - + + Theorems/Nat - -Theorems/Nat + +Theorems/Nat Types/Nat->Theorems/Nat - - + + - + Modal/Etale - -Modal/Etale + +Modal/Etale - + Modal/Disc->Modal/Etale - - + + Algebra/Basic - -Algebra/Basic + +Algebra/Basic Algebra/Category - -Algebra/Category + +Algebra/Category Algebra/Basic->Algebra/Category - - + + Algebra/Monoid - -Algebra/Monoid + +Algebra/Monoid Algebra/Basic->Algebra/Monoid - - + + Algebra/Geometry - -Algebra/Geometry + +Algebra/Geometry Algebra/Basic->Algebra/Geometry - - + + Algebra/Group/Basic - -Algebra/Group/Basic + +Algebra/Group/Basic Algebra/Basic->Algebra/Group/Basic - - + + Algebra/EilenbergMacLane - -Algebra/EilenbergMacLane + +Algebra/EilenbergMacLane Algebra/Group/Basic->Algebra/EilenbergMacLane - - + + Algebra/Group/Absolutizer - -Algebra/Group/Absolutizer + +Algebra/Group/Absolutizer Algebra/Group/Basic->Algebra/Group/Absolutizer - - + + Algebra/Group/Automorphism - -Algebra/Group/Automorphism + +Algebra/Group/Automorphism Algebra/Group/Basic->Algebra/Group/Automorphism - - + + Algebra/Group/Finite - -Algebra/Group/Finite + +Algebra/Group/Finite Algebra/Group/Basic->Algebra/Group/Finite - - + + Algebra/Group/Free - -Algebra/Group/Free + +Algebra/Group/Free Algebra/Group/Basic->Algebra/Group/Free - - + + Algebra/Group/Periodic - -Algebra/Group/Periodic + +Algebra/Group/Periodic Algebra/Group/Basic->Algebra/Group/Periodic - - + + Algebra/Group/Product - -Algebra/Group/Product + +Algebra/Group/Product Algebra/Group/Basic->Algebra/Group/Product - - + + Algebra/Group/Subgroup - -Algebra/Group/Subgroup + +Algebra/Group/Subgroup Algebra/Group/Basic->Algebra/Group/Subgroup - - + + Algebra/Boolean - -Algebra/Boolean + +Algebra/Boolean Algebra/Orgraph - -Algebra/Orgraph + +Algebra/Orgraph Algebra/Reals - -Algebra/Reals + +Algebra/Reals Algebra/Orgraph->Algebra/Reals - - + + Algebra/Group/Limited - -Algebra/Group/Limited + +Algebra/Group/Limited Algebra/Reals->Algebra/Group/Limited - - + + HITs/Topologization - -HITs/Topologization + +HITs/Topologization Algebra/Reals->HITs/Topologization - - + + Algebra/Ring - -Algebra/Ring + +Algebra/Ring Algebra/Ring->Algebra/Boolean - - + + Algebra/Ring->Algebra/Orgraph - - + + Algebra/Transformational - -Algebra/Transformational + +Algebra/Transformational Algebra/Group/Action - -Algebra/Group/Action + +Algebra/Group/Action Algebra/Group/Action->Algebra/Transformational - - + + Algebra/Group/Alternating - -Algebra/Group/Alternating + +Algebra/Group/Alternating Algebra/Group/Semidirect - -Algebra/Group/Semidirect + +Algebra/Group/Semidirect Algebra/Group/Automorphism->Algebra/Group/Semidirect - - + + Algebra/Group/Presentation - -Algebra/Group/Presentation + +Algebra/Group/Presentation Algebra/Group/Free->Algebra/Group/Presentation - - + + Algebra/Group/Product->Algebra/Transformational - - + + Algebra/Group/Differential - -Algebra/Group/Differential + +Algebra/Group/Differential Algebra/Group/Subgroup->Algebra/Group/Differential - - + + Algebra/Group/Factor - -Algebra/Group/Factor + +Algebra/Group/Factor Algebra/Group/Subgroup->Algebra/Group/Factor - - + + Algebra/Group/Lemmas - -Algebra/Group/Lemmas + +Algebra/Group/Lemmas Algebra/Group/Subgroup->Algebra/Group/Lemmas - - + + Algebra/Group/Symmetric - -Algebra/Group/Symmetric + +Algebra/Group/Symmetric Algebra/Group/Subgroup->Algebra/Group/Symmetric - - + + Algebra/Group/Factor->Algebra/Ring - - + + Algebra/Group/Factor->Algebra/Group/Alternating - - + + Algebra/Group/Isomorphism - -Algebra/Group/Isomorphism + +Algebra/Group/Isomorphism Algebra/Group/Factor->Algebra/Group/Isomorphism - - + + Algebra/Group/Isomorphism->Algebra/Group/Presentation - - + + Algebra/Group/Symmetric->Algebra/Group/Limited - - + + Algebra/Group/Symmetric->Algebra/Group/Action - - + + Algebra/Group/Symmetric->Algebra/Group/Isomorphism - - + + Algebra/Group/Z - -Algebra/Group/Z + +Algebra/Group/Z Algebra/Group/Symmetric->Algebra/Group/Z - - + + Types/Category - -Types/Category + +Types/Category Types/Coproduct->Structures - - + + Types/Ens - -Types/Ens + +Types/Ens Types/Ens->Algebra/Basic - - + + Types/Setquot - -Types/Setquot + +Types/Setquot Types/Ens->Types/Setquot - - + + HITs/Graph - -HITs/Graph + +HITs/Graph Types/HEq->HITs/Graph - - + + Theorems/Funext - -Theorems/Funext + +Theorems/Funext Types/HEq->Theorems/Funext - - + + - + Modal/Infinitesimal->Modal/Disc - - + + Types/Unit->Structures - - + + HITs/Suspension - -HITs/Suspension + +HITs/Suspension Types/Unit->HITs/Suspension - - + + HITs/Wedge - -HITs/Wedge + +HITs/Wedge Types/Unit->HITs/Wedge - - + + Types/Sigma->Structures - - + + - + HITs/Coequalizer - -HITs/Coequalizer + +HITs/Coequalizer - + HITs/Graph->HITs/Coequalizer - - + + - + HITs/Colimit - -HITs/Colimit + +HITs/Colimit - + HITs/Graph->HITs/Colimit - - + + - + HITs/Generalized - -HITs/Generalized + +HITs/Generalized - + HITs/Graph->HITs/Generalized - - + + - + HITs/Pushout - -HITs/Pushout + +HITs/Pushout - + HITs/Graph->HITs/Pushout - - + + Types/Product - -Types/Product + +Types/Product - + Theorems/Funext->Types/Product - - + + Types/Integer - -Types/Integer + +Types/Integer HITs/Circle - -HITs/Circle + +HITs/Circle Types/Integer->HITs/Circle - - + + HITs/Circle->Algebra/Group/Z - - + + Theorems/Hopf - -Theorems/Hopf + +Theorems/Hopf HITs/Circle->Theorems/Hopf - - + + HITs/Moebius - -HITs/Moebius + +HITs/Moebius HITs/Circle->HITs/Moebius - - + + HITs/Reals - -HITs/Reals + +HITs/Reals HITs/Circle->HITs/Reals - - + + + + + +HITs/Sphere + +HITs/Sphere + + + +HITs/Circle->HITs/Sphere + + - + Theorems/Nat->Algebra/Reals - - + + - + Theorems/Nat->Algebra/Group/Finite - - + + - + Theorems/Nat->Algebra/Group/Lemmas - - + + - + Theorems/Nat->Types/Integer - - + + - + HITs/Int - -HITs/Int + +HITs/Int - + Theorems/Nat->HITs/Int - - + + Types/Precategory - -Types/Precategory + +Types/Precategory Types/Precategory->Types/Category - - + + Types/Product->Structures - - + + - + HITs/Suspension->Algebra/EilenbergMacLane - - + + - + HITs/Suspension->HITs/Circle - - + + - + HITs/Join - -HITs/Join + +HITs/Join - + HITs/Suspension->HITs/Join - - + + - + HITs/Flattening - -HITs/Flattening + +HITs/Flattening - + HITs/Coequalizer->HITs/Flattening - - + + - + HITs/Colimit->HITs/Merely - - + + - + HITs/Colimit->Types/Nat - - + + - + HITs/Generalized->HITs/Merely - - + + - + HITs/Pushout->HITs/Suspension - - + + - + HITs/Pushout->HITs/Wedge - - + + - + Cubical/Square - -Cubical/Square + +Cubical/Square - + Cubical/Cubes->Cubical/Square - - + + - + Cubical/Connection - -Cubical/Connection + +Cubical/Connection - + Cubical/Path->Cubical/Connection - - + + - + Cubical/Path->Cubical/Square - - + + - + Cubical/V - -Cubical/V + +Cubical/V - + Cubical/Path->Cubical/V - - + + - + Theorems/Equiv->Types/Precategory - - + + - + Theorems/Univalence - -Theorems/Univalence + +Theorems/Univalence - + Theorems/Equiv->Theorems/Univalence - - + + - + Theorems/Pullback - -Theorems/Pullback + +Theorems/Pullback - + Theorems/Equiv->Theorems/Pullback - - + + - + Theorems/Fibration->Theorems/Hopf - - + + - + HITs/Trunc->Algebra/Monoid - - + + - + HITs/Trunc->Algebra/EilenbergMacLane - - + + - + HITs/Quotient - -HITs/Quotient + +HITs/Quotient - + HITs/Trunc->HITs/Quotient - - + + - + Theorems/Connectedness - -Theorems/Connectedness + +Theorems/Connectedness - + HITs/Trunc->Theorems/Connectedness - - + + - + Theorems/Functions->Types/Precategory - - + + - + Theorems/Functions->Modal/Etale - - + + - + Theorems/Functions->Theorems/Univalence - - + + - + HITs/Quotient->Algebra/Group/Absolutizer - - + + - + HITs/Quotient->Algebra/Group/Action - - + + - + HITs/Quotient->Algebra/Group/Factor - - + + - + Cubical/Example - -Cubical/Example + +Cubical/Example - + Cubical/V->Cubical/Example - - + + - + Meta/Basic - -Meta/Basic + +Meta/Basic - + Meta/Basic->Proto - - + + - + Meta/HottTheory - -Meta/HottTheory + +Meta/HottTheory - + Meta/HottTheory->Meta/Basic - - + + - + Meta/Notation - -Meta/Notation + +Meta/Notation - + Meta/Notation->Meta/Basic - - + + - + Meta/Tactic - -Meta/Tactic + +Meta/Tactic - + Meta/Tactic->Meta/Basic - - + + - + Theorems/Classical - -Theorems/Classical + +Theorems/Classical - + Theorems/Classical->Algebra/Category - - + + - + Theorems/Classical->Algebra/Orgraph - - + + - + Theorems/Univalence->Types/Ens - - + + - + Theorems/Univalence->HITs/Circle - - + + - + Theorems/Univalence->Theorems/Nat - - + + - + Theorems/Univalence->HITs/Flattening - - + + - + Theorems/Univalence->Theorems/Connectedness - - + + - + Theorems/Univalence->Cubical/V - - + + - + Theorems/Univalence->Theorems/Classical - - + +