Define left half-smash products

references.bib

@@ -28,6 +28,15 @@ @article{AKS15
   langid      = {english}
 }
 
+@misc{Lavenir23,
+      title={Hilton-Milnor's theorem in $\infty$-topoi},
+      author={Samuel Lavenir},
+      year={2023},
+      eprint={2312.12370},
+      archivePrefix={arXiv},
+      primaryClass={math.AT},
+}
+
 @misc{Anel24,
   title         = {The category of $\pi$-finite spaces},
   author        = {Mathieu Anel},

src/foundation/unit-type.lagda.md

@@ -129,7 +129,10 @@ module _
     is-contr-retraction-terminal-map (retraction-is-equiv H)
 
   is-contr-equiv-unit : A ≃ unit → is-contr A
-  is-contr-equiv-unit e = map-inv-equiv e star , is-retraction-map-inv-equiv e
+  is-contr-equiv-unit e = (map-inv-equiv e star , is-retraction-map-inv-equiv e)
+
+  is-contr-equiv-unit' : unit ≃ A → is-contr A
+  is-contr-equiv-unit' e = (map-equiv e star , is-section-map-inv-equiv e)
 ```
 
 ### Any contractible type is equivalent to the raised unit type

src/synthetic-homotopy-theory.lagda.md

@@ -23,7 +23,8 @@ open import synthetic-homotopy-theory.cocones-under-sequential-diagrams public
 open import synthetic-homotopy-theory.cocones-under-spans public
 open import synthetic-homotopy-theory.codiagonals-of-maps public
 open import synthetic-homotopy-theory.coequalizers public
-open import synthetic-homotopy-theory.cofibers public
+open import synthetic-homotopy-theory.cofibers-of-maps public
+open import synthetic-homotopy-theory.cofibers-of-pointed-maps public
 open import synthetic-homotopy-theory.coforks public
 open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams public
 open import synthetic-homotopy-theory.conjugation-loops public
@@ -84,6 +85,7 @@ open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types publ
 open import synthetic-homotopy-theory.join-powers-of-types public
 open import synthetic-homotopy-theory.joins-of-maps public
 open import synthetic-homotopy-theory.joins-of-types public
+open import synthetic-homotopy-theory.left-half-smash-products public
 open import synthetic-homotopy-theory.loop-homotopy-circle public
 open import synthetic-homotopy-theory.loop-spaces public
 open import synthetic-homotopy-theory.maps-of-prespectra public

src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md

@@ -0,0 +1,134 @@
+# Cofibers of maps
+
+```agda
+module synthetic-homotopy-theory.cofibers-of-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.constant-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+open import structured-types.pointed-unit-type
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
+open import synthetic-homotopy-theory.dependent-universal-property-pushouts
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "cofiber" Disambiguation="of a map of types" WD="mapping cone" WDID=Q306560 Agda=cofiber}}
+of a map `f : A → B` is the [pushout](synthetic-homotopy-theory.pushouts.md) of
+the span `B ← A → *`.
+
+## Definitions
+
+### The cofiber of a map
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  cofiber : UU (l1 ⊔ l2)
+  cofiber = pushout f (terminal-map A)
+
+  cocone-cofiber : cocone f (terminal-map A) cofiber
+  cocone-cofiber = cocone-pushout f (terminal-map A)
+
+  inl-cofiber : B → cofiber
+  inl-cofiber = pr1 cocone-cofiber
+
+  inr-cofiber : unit → cofiber
+  inr-cofiber = pr1 (pr2 cocone-cofiber)
+
+  point-cofiber : cofiber
+  point-cofiber = inr-cofiber star
+
+  pointed-type-cofiber : Pointed-Type (l1 ⊔ l2)
+  pointed-type-cofiber = (cofiber , point-cofiber)
+
+  inr-pointed-map-cofiber : unit-Pointed-Type →∗ pointed-type-cofiber
+  inr-pointed-map-cofiber = inclusion-point-Pointed-Type (pointed-type-cofiber)
+
+  universal-property-cofiber :
+    universal-property-pushout f (terminal-map A) cocone-cofiber
+  universal-property-cofiber = up-pushout f (terminal-map A)
+
+  dependent-universal-property-cofiber :
+    dependent-universal-property-pushout f (terminal-map A) cocone-cofiber
+  dependent-universal-property-cofiber = dup-pushout f (terminal-map A)
+
+  cogap-cofiber :
+    {l : Level} {X : UU l} → cocone f (terminal-map A) X → cofiber → X
+  cogap-cofiber = cogap f (terminal-map A)
+
+  dependent-cogap-cofiber :
+    {l : Level} {P : cofiber → UU l}
+    (c : dependent-cocone f (terminal-map A) (cocone-cofiber) P)
+    (x : cofiber) → P x
+  dependent-cogap-cofiber = dependent-cogap f (terminal-map A)
+```
+
+## Properties
+
+### The cofiber of an equivalence is contractible
+
+Note that this is not a logical equivalence. Not every map whose cofibers are
+all contractible is an equivalence. For instance, the cofiber of `X → 1` where
+`X` is an [acyclic type](synthetic-homotopy-theory.acyclic-types.md) is by
+definition contractible. Examples of noncontractible acyclic types include
+[Hatcher's acyclic type](synthetic-homotopy-theory.hatchers-acyclic-type.md).
+
+```agda
+is-contr-cofiber-is-equiv :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
+  is-equiv f → is-contr (cofiber f)
+is-contr-cofiber-is-equiv {A = A} f is-equiv-f =
+  is-contr-equiv-unit'
+    ( inr-cofiber f ,
+      is-equiv-universal-property-pushout
+        ( f)
+        ( terminal-map A)
+        ( cocone-cofiber f)
+        ( is-equiv-f)
+        ( universal-property-cofiber f))
+```
+
+### The cofibers of the point inclusions in `B` are equivalent to `B`
+
+```agda
+module _
+  {l : Level} {B : UU l} (b : B)
+  where
+
+  is-equiv-inl-cofiber-point : is-equiv (inl-cofiber (point b))
+  is-equiv-inl-cofiber-point =
+    is-equiv-universal-property-pushout'
+      ( point b)
+      ( terminal-map unit)
+      ( cocone-pushout (point b) (terminal-map unit))
+      ( is-equiv-is-contr (terminal-map unit) is-contr-unit is-contr-unit)
+      ( up-pushout (point b) (terminal-map unit))
+
+  compute-cofiber-point : B ≃ cofiber (point b)
+  compute-cofiber-point = (inl-cofiber (point b) , is-equiv-inl-cofiber-point)
+```
+
+## See also
+
+- Cofibers of maps are formally dual to
+  [fibers of maps](foundation-core.fibers-of-maps.md)

src/synthetic-homotopy-theory/cofibers-of-pointed-maps.lagda.md

@@ -0,0 +1,78 @@
+# Cofibers of pointed maps
+
+```agda
+module synthetic-homotopy-theory.cofibers-of-pointed-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.constant-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+open import structured-types.pointed-unit-type
+
+open import synthetic-homotopy-theory.cocones-under-pointed-span-diagrams
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.cofibers-of-maps
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
+open import synthetic-homotopy-theory.dependent-universal-property-pushouts
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.pushouts-of-pointed-types
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "cofiber" Disambiguation="of a pointed map of pointed types" WD="mapping cone" WDID=Q306560 Agda=cofiber-Pointed-Type}}
+of a [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` is the
+[pushout](synthetic-homotopy-theory.pushouts-of-pointed-types.md) of the span of
+pointed maps `1 ← A → B`.
+
+## Definitions
+
+### The cofiber of a pointed map
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
+  where
+
+  type-cofiber-Pointed-Type : UU (l1 ⊔ l2)
+  type-cofiber-Pointed-Type =
+    type-pushout-Pointed-Type f (terminal-pointed-map A)
+
+  point-cofiber-Pointed-Type : Pointed-Type (l1 ⊔ l2)
+  point-cofiber-Pointed-Type = pushout-Pointed-Type f (terminal-pointed-map A)
+
+  cofiber-Pointed-Type : Pointed-Type (l1 ⊔ l2)
+  cofiber-Pointed-Type = pushout-Pointed-Type f (terminal-pointed-map A)
+
+  inl-cofiber-Pointed-Type : B →∗ cofiber-Pointed-Type
+  inl-cofiber-Pointed-Type = inl-pushout-Pointed-Type f (terminal-pointed-map A)
+
+  inr-cofiber-Pointed-Type : unit-Pointed-Type →∗ cofiber-Pointed-Type
+  inr-cofiber-Pointed-Type = inr-pushout-Pointed-Type f (terminal-pointed-map A)
+
+  map-cogap-cofiber-Pointed-Type :
+    {l : Level} {X : Pointed-Type l} →
+    cocone-Pointed-Type f (terminal-pointed-map A) X →
+    type-cofiber-Pointed-Type → type-Pointed-Type X
+  map-cogap-cofiber-Pointed-Type =
+    map-cogap-Pointed-Type f (terminal-pointed-map A)
+
+  cogap-cofiber-Pointed-Type :
+    {l : Level} {X : Pointed-Type l} →
+    cocone-Pointed-Type f (terminal-pointed-map A) X →
+    cofiber-Pointed-Type →∗ X
+  cogap-cofiber-Pointed-Type = cogap-Pointed-Type f (terminal-pointed-map A)
+```