Pi4S3 Paper (#1151)

* t * duplicate * wups * rme * ganea stuff * w * w * w * stuff * stuff * fixes * fixes * fixes * added comment
agda · Sep 2, 2024 · e2cf0ab · e2cf0ab
1 parent 1011201
commit e2cf0ab
Show file tree

Hide file tree

Showing 9 changed files with 2,143 additions and 2 deletions.
diff --git a/Cubical/HITs/Join/Base.agda b/Cubical/HITs/Join/Base.agda
@@ -4,6 +4,7 @@ module Cubical.HITs.Join.Base where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed.Base
 
 open import Cubical.HITs.S1
 open import Cubical.HITs.S3
@@ -15,6 +16,11 @@ data join {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') wh
   inr : B → join A B
   push : ∀ a b → inl a ≡ inr b
 
+join∙ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
+  → Pointed _
+fst (join∙ A B) = join (fst A) (fst B)
+snd (join∙ A B) = inl (pt A)
+
 facek01 : I → I → I → join S¹ S¹
 facek01 i j k = hfill (λ l → λ { (j = i0) → push base base (~ l ∧ ~ k)
                                ; (j = i1) → push base base (~ l ∧ ~ k)

diff --git a/Cubical/HITs/SmashProduct/Base.agda b/Cubical/HITs/SmashProduct/Base.agda