From 147d5c9d8e15fd23c84862b1538925afbdebe501 Mon Sep 17 00:00:00 2001
From: maybemabeline <142519092+maybemabeline@users.noreply.github.com>
Date: Tue, 31 Oct 2023 13:53:13 +0100
Subject: [PATCH] Universal property of smash products (#865)

I added some functions for computing with the universal property of
pushouts of pointed types and a function that computes the
identifications created by the map from the product to the smash
product.
I also started working on one of the sides of the universal property,
but the last hole ended up as a very complicated dependent
identification that I'm not sure how to handle. If anyone wants to look
at it, you are welcome to do so :)

---------

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 .../equality-dependent-pair-types.lagda.md    |   8 +
 src/foundation/homotopies.lagda.md            |  45 ++-
 ...commuting-squares-of-pointed-maps.lagda.md |  24 +-
 .../pointed-homotopies.lagda.md               |   2 +
 .../pointed-unit-type.lagda.md                |  31 +-
 .../pushouts-of-pointed-types.lagda.md        |  39 +++
 .../smash-products-of-pointed-types.lagda.md  | 274 +++++++++++++++++-
 .../wedges-of-pointed-types.lagda.md          |  65 +++++
 8 files changed, 450 insertions(+), 38 deletions(-)

diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md
index 4c48dcb81a..4b812e58ea 100644
--- a/src/foundation-core/equality-dependent-pair-types.lagda.md
+++ b/src/foundation-core/equality-dependent-pair-types.lagda.md
@@ -105,6 +105,14 @@ module _
 
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
   η-pair t = eq-pair-Σ refl refl
+
+  eq-base-eq-pair : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
+  eq-base-eq-pair p = pr1 (pair-eq-Σ p)
+
+  dependent-eq-family-eq-pair :
+    {s t : Σ A B} → (p : s ＝ t) →
+    dependent-identification B (eq-base-eq-pair p) (pr2 s) (pr2 t)
+  dependent-eq-family-eq-pair p = pr2 (pair-eq-Σ p)
 ```
 
 ### Lifting equality to the total space
diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
index 2d9062cd1d..7f448ae5b2 100644
--- a/src/foundation/homotopies.lagda.md
+++ b/src/foundation/homotopies.lagda.md
@@ -20,6 +20,7 @@ open import foundation.identity-types
 open import foundation.path-algebra
 open import foundation.universe-levels
 
+open import foundation-core.dependent-identifications
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-function-types
@@ -208,12 +209,19 @@ module _
 
   compute-dependent-identification-eq-value :
     {x y : A} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
-    (((apd f p) ∙ r) ＝ ((ap (tr B p) q) ∙ (apd g p))) ≃
-    (tr (eq-value f g) p q ＝ r)
+    coherence-square-identifications (ap (tr B p) q) (apd f p) (apd g p) r ≃
+    dependent-identification (eq-value f g) p q r
   pr1 (compute-dependent-identification-eq-value p q r) =
     map-compute-dependent-identification-eq-value f g p q r
   pr2 (compute-dependent-identification-eq-value p q r) =
     is-equiv-map-compute-dependent-identification-eq-value p q r
+
+  inv-map-compute-dependent-identification-eq-value :
+    {x y : A} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
+    dependent-identification (eq-value f g) p q r →
+    coherence-square-identifications (ap (tr B p) q) (apd f p) (apd g p) r
+  inv-map-compute-dependent-identification-eq-value p q r =
+    map-inv-equiv (compute-dependent-identification-eq-value p q r)
 ```
 
 ### Computing dependent-identifications in the type family `eq-value` of ordinary functions
@@ -224,23 +232,30 @@ module _
   where
 
   is-equiv-map-compute-dependent-identification-eq-value-function :
-    {x y : A} (p : x ＝ y) (q : eq-value f g x) (q' : eq-value f g y) →
-    is-equiv (map-compute-dependent-identification-eq-value-function f g p q q')
-  is-equiv-map-compute-dependent-identification-eq-value-function refl q q' =
+    {x y : A} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
+    is-equiv (map-compute-dependent-identification-eq-value-function f g p q r)
+  is-equiv-map-compute-dependent-identification-eq-value-function refl q r =
     is-equiv-comp
       ( inv)
-      ( concat' q' right-unit)
-      ( is-equiv-concat' q' right-unit)
-      ( is-equiv-inv q' q)
+      ( concat' r right-unit)
+      ( is-equiv-concat' r right-unit)
+      ( is-equiv-inv r q)
 
   compute-dependent-identification-eq-value-function :
-    {a0 a1 : A} (p : a0 ＝ a1) (q : f a0 ＝ g a0) (q' : f a1 ＝ g a1) →
-    ( coherence-square-identifications q (ap f p) (ap g p) q') ≃
-    ( tr (eq-value f g) p q ＝ q')
-  pr1 (compute-dependent-identification-eq-value-function p q q') =
-    map-compute-dependent-identification-eq-value-function f g p q q'
-  pr2 (compute-dependent-identification-eq-value-function p q q') =
-    is-equiv-map-compute-dependent-identification-eq-value-function p q q'
+    {x y : A} (p : x ＝ y) (q : f x ＝ g x) (r : f y ＝ g y) →
+    coherence-square-identifications q (ap f p) (ap g p) r ≃
+    dependent-identification (eq-value f g) p q r
+  pr1 (compute-dependent-identification-eq-value-function p q r) =
+    map-compute-dependent-identification-eq-value-function f g p q r
+  pr2 (compute-dependent-identification-eq-value-function p q r) =
+    is-equiv-map-compute-dependent-identification-eq-value-function p q r
+
+  inv-map-compute-dependent-identification-eq-value-function :
+    {x y : A} (p : x ＝ y) (q : f x ＝ g x) (r : f y ＝ g y) →
+    dependent-identification (eq-value f g) p q r →
+    coherence-square-identifications q (ap f p) (ap g p) r
+  inv-map-compute-dependent-identification-eq-value-function p q r =
+    map-inv-equiv (compute-dependent-identification-eq-value-function p q r)
 ```
 
 ### Relation between between `compute-dependent-identification-eq-value-function` and `nat-htpy`
diff --git a/src/structured-types/commuting-squares-of-pointed-maps.lagda.md b/src/structured-types/commuting-squares-of-pointed-maps.lagda.md
index a49e3d8c0b..b08a0228db 100644
--- a/src/structured-types/commuting-squares-of-pointed-maps.lagda.md
+++ b/src/structured-types/commuting-squares-of-pointed-maps.lagda.md
@@ -7,6 +7,8 @@ module structured-types.commuting-squares-of-pointed-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.function-types
 open import foundation.universe-levels
 
 open import structured-types.pointed-homotopies
@@ -35,12 +37,24 @@ between the pointedness preservation proofs.
 ## Definition
 
 ```agda
-coherence-square-pointed-maps :
+module _
   {l1 l2 l3 l4 : Level}
   {A : Pointed-Type l1} {B : Pointed-Type l2}
   {C : Pointed-Type l3} {X : Pointed-Type l4}
-  (top : C →∗ B) (left : C →∗ A) (right : B →∗ X) (bottom : A →∗ X) →
-  UU (l3 ⊔ l4)
-coherence-square-pointed-maps top left right bottom =
-  (bottom ∘∗ left) ~∗ (right ∘∗ top)
+  (top : C →∗ B) (left : C →∗ A) (right : B →∗ X) (bottom : A →∗ X)
+  where
+
+  coherence-square-pointed-maps : UU (l3 ⊔ l4)
+  coherence-square-pointed-maps =
+    bottom ∘∗ left ~∗ right ∘∗ top
+
+  coherence-square-maps-coherence-square-pointed-maps :
+    coherence-square-pointed-maps →
+    coherence-square-maps
+      ( map-pointed-map top)
+      ( map-pointed-map left)
+      ( map-pointed-map right)
+      ( map-pointed-map bottom)
+  coherence-square-maps-coherence-square-pointed-maps =
+    htpy-pointed-htpy (bottom ∘∗ left) (right ∘∗ top)
 ```
diff --git a/src/structured-types/pointed-homotopies.lagda.md b/src/structured-types/pointed-homotopies.lagda.md
index 0276d4347f..25b71c6a97 100644
--- a/src/structured-types/pointed-homotopies.lagda.md
+++ b/src/structured-types/pointed-homotopies.lagda.md
@@ -79,6 +79,8 @@ _~∗_ :
   pointed-Π A B → pointed-Π A B → UU (l1 ⊔ l2)
 _~∗_ {A = A} {B} = htpy-pointed-Π
 
+infix 6 _~∗_
+
 htpy-pointed-htpy :
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
   (f g : pointed-Π A B) → f ~∗ g →
diff --git a/src/structured-types/pointed-unit-type.lagda.md b/src/structured-types/pointed-unit-type.lagda.md
index fa2cb1ce59..af2130cf0b 100644
--- a/src/structured-types/pointed-unit-type.lagda.md
+++ b/src/structured-types/pointed-unit-type.lagda.md
@@ -12,6 +12,7 @@ open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import structured-types.pointed-homotopies
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
 ```
@@ -33,12 +34,26 @@ pr2 unit-Pointed-Type = star
 ## Properties
 
 ```agda
-terminal-pointed-map : {l : Level} (X : Pointed-Type l) → X →∗ unit-Pointed-Type
-pr1 (terminal-pointed-map X) _ = star
-pr2 (terminal-pointed-map X) = refl
-
-inclusion-point-Pointed-Type :
-  {l : Level} (X : Pointed-Type l) → unit-Pointed-Type →∗ X
-pr1 (inclusion-point-Pointed-Type X) = point (point-Pointed-Type X)
-pr2 (inclusion-point-Pointed-Type X) = refl
+module _
+  {l : Level} (X : Pointed-Type l)
+  where
+
+  terminal-pointed-map : X →∗ unit-Pointed-Type
+  pr1 terminal-pointed-map _ = star
+  pr2 terminal-pointed-map = refl
+
+  map-terminal-pointed-map : type-Pointed-Type X → unit
+  map-terminal-pointed-map =
+    map-pointed-map {A = X} {B = unit-Pointed-Type}
+      terminal-pointed-map
+
+  inclusion-point-Pointed-Type :
+    unit-Pointed-Type →∗ X
+  pr1 inclusion-point-Pointed-Type = point (point-Pointed-Type X)
+  pr2 inclusion-point-Pointed-Type = refl
+
+  is-initial-unit-Pointed-Type :
+    ( f : unit-Pointed-Type →∗ X) → f ~∗ inclusion-point-Pointed-Type
+  pr1 (is-initial-unit-Pointed-Type f) _ = preserves-point-pointed-map f
+  pr2 (is-initial-unit-Pointed-Type f) = inv right-unit
 ```
diff --git a/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md
index 3ddcacfc23..cf1a1ffbe8 100644
--- a/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md
@@ -115,3 +115,42 @@ module _
     ( preserves-point-pointed-map
       ( horizontal-pointed-map-cocone-Pointed-Type f g c))
 ```
+
+### Computation with the cogap map for pointed types
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level}
+  {S : Pointed-Type l1} {A : Pointed-Type l2} {B : Pointed-Type l3}
+  ( f : S →∗ A) (g : S →∗ B)
+  { X : Pointed-Type l4} (c : type-cocone-Pointed-Type f g X)
+  where
+
+  compute-inl-cogap-Pointed-Type :
+    ( x : type-Pointed-Type A) →
+    ( map-cogap-Pointed-Type
+      ( f)
+      ( g)
+      ( c)
+      ( map-pointed-map (inl-pushout-Pointed-Type f g) x)) ＝
+    ( horizontal-map-cocone-Pointed-Type f g c x)
+  compute-inl-cogap-Pointed-Type =
+    compute-inl-cogap
+      ( map-pointed-map f)
+      ( map-pointed-map g)
+      ( cocone-type-cocone-Pointed-Type f g c)
+
+  compute-inr-cogap-Pointed-Type :
+    ( y : type-Pointed-Type B) →
+    ( map-cogap-Pointed-Type
+      ( f)
+      ( g)
+      ( c)
+      ( map-pointed-map (inr-pushout-Pointed-Type f g) y)) ＝
+    ( vertical-map-cocone-Pointed-Type f g c y)
+  compute-inr-cogap-Pointed-Type =
+    compute-inr-cogap
+      ( map-pointed-map f)
+      ( map-pointed-map g)
+      ( cocone-type-cocone-Pointed-Type f g c)
+```
diff --git a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
index 2cf1d0ac32..8fa69c7b96 100644
--- a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
@@ -7,15 +7,29 @@ module synthetic-homotopy-theory.smash-products-of-pointed-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.path-algebra
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies
 
 open import structured-types.pointed-cartesian-product-types
+open import structured-types.pointed-families-of-types
+open import structured-types.pointed-homotopies
 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-of-pointed-types
+open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.pushouts-of-pointed-types
 open import synthetic-homotopy-theory.wedges-of-pointed-types
 ```
@@ -88,19 +102,26 @@ map-cogap-smash-prod-Pointed-Type c =
 
 ## Properties
 
-### The canonical pointed map from the product to the smash product
+### The canonical pointed map from the cartesian product to the smash product
 
 ```agda
-pointed-map-smash-prod-prod-Pointed-Type :
-  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
-  (A ×∗ B) →∗ (A ∧∗ B)
-pointed-map-smash-prod-prod-Pointed-Type A B =
-  inl-pushout-Pointed-Type
-    ( pointed-map-prod-wedge-Pointed-Type A B)
-    ( terminal-pointed-map (A ∨∗ B))
+module _
+  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
+  where
+
+  pointed-map-smash-prod-prod-Pointed-Type : (A ×∗ B) →∗ (A ∧∗ B)
+  pointed-map-smash-prod-prod-Pointed-Type =
+    inl-pushout-Pointed-Type
+      ( pointed-map-prod-wedge-Pointed-Type A B)
+      ( terminal-pointed-map (A ∨∗ B))
+
+  map-smash-prod-prod-Pointed-Type :
+    type-Pointed-Type (A ×∗ B) → type-Pointed-Type (A ∧∗ B)
+  map-smash-prod-prod-Pointed-Type =
+    map-pointed-map pointed-map-smash-prod-prod-Pointed-Type
 ```
 
-### The smash product is the product in the category of pointed types
+### Pointed maps into pointed types `A` and `B` induce a pointed map into `A ∧∗ B`
 
 ```agda
 module _
@@ -120,7 +141,240 @@ module _
     pr1 (gap-smash-prod-Pointed-Type f g)
 ```
 
-It remains to show that this is the correct map, and that it is unique.
+### The canonical map from the wedge sum to the smash product identifies all points
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
+  where
+
+  pointed-map-smash-prod-wedge-Pointed-Type : (A ∨∗ B) →∗ (A ∧∗ B)
+  pointed-map-smash-prod-wedge-Pointed-Type =
+    pointed-map-smash-prod-prod-Pointed-Type A B ∘∗
+    pointed-map-prod-wedge-Pointed-Type A B
+
+  map-smash-prod-wedge-Pointed-Type :
+    type-Pointed-Type (A ∨∗ B) → type-Pointed-Type (A ∧∗ B)
+  map-smash-prod-wedge-Pointed-Type =
+    map-pointed-map pointed-map-smash-prod-wedge-Pointed-Type
+
+  contraction-map-smash-prod-wedge-Pointed-Type :
+    ( x : type-Pointed-Type (A ∨∗ B)) →
+    map-smash-prod-wedge-Pointed-Type x ＝
+    point-Pointed-Type (A ∧∗ B)
+  contraction-map-smash-prod-wedge-Pointed-Type x =
+    ( glue-pushout
+      ( map-prod-wedge-Pointed-Type A B)
+      ( map-pointed-map {A = A ∨∗ B} {B = unit-Pointed-Type}
+        ( terminal-pointed-map (A ∨∗ B)))
+      ( x)) ∙
+    ( htpy-right-whisk
+      ( htpy-pointed-htpy
+        ( inr-pushout-Pointed-Type
+          ( pointed-map-prod-wedge-Pointed-Type A B)
+          ( terminal-pointed-map (A ∨∗ B)))
+        ( inclusion-point-Pointed-Type (A ∧∗ B))
+        ( is-initial-unit-Pointed-Type
+          ( A ∧∗ B)
+          ( inr-pushout-Pointed-Type
+            ( pointed-map-prod-wedge-Pointed-Type A B)
+            ( terminal-pointed-map (A ∨∗ B)))))
+      ( map-terminal-pointed-map (A ∨∗ B))
+      ( x)) ∙
+    ( preserves-point-pointed-map
+      ( inclusion-point-Pointed-Type (A ∧∗ B)))
+
+  coh-contraction-map-smash-prod-wedge-Pointed-Type :
+    ( ap
+      ( map-smash-prod-wedge-Pointed-Type)
+      ( glue-wedge-Pointed-Type A B)) ∙
+    ( contraction-map-smash-prod-wedge-Pointed-Type
+        ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))) ＝
+    ( contraction-map-smash-prod-wedge-Pointed-Type
+      ( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
+  coh-contraction-map-smash-prod-wedge-Pointed-Type =
+    ( inv-map-compute-dependent-identification-eq-value-function
+      ( map-smash-prod-wedge-Pointed-Type)
+      ( map-pointed-map
+        ( constant-pointed-map (A ∨∗ B) (A ∧∗ B)))
+      ( glue-wedge-Pointed-Type A B)
+      ( contraction-map-smash-prod-wedge-Pointed-Type
+        ( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
+      ( contraction-map-smash-prod-wedge-Pointed-Type
+        ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B)))
+      ( apd
+        ( contraction-map-smash-prod-wedge-Pointed-Type)
+        ( glue-wedge-Pointed-Type A B))) ∙
+    ( identification-left-whisk
+      ( contraction-map-smash-prod-wedge-Pointed-Type
+        ( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
+      ( ap-const
+        ( point-Pointed-Type (A ∧∗ B))
+        ( glue-wedge-Pointed-Type A B))) ∙
+    ( right-unit)
+```
+
+### The map from the pointed product to the smash product identifies elements
+
+of the form `(x, b)` and `(a, y)`, where `b` and `a` are the base points of `B`
+and `A` respectively.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Pointed-Type l1) (B : Pointed-Type l2)
+  where
+
+  inl-glue-smash-prod-Pointed-Type :
+    ( x : type-Pointed-Type A) →
+    map-smash-prod-prod-Pointed-Type A B
+      ( x , point-Pointed-Type B) ＝
+    map-smash-prod-prod-Pointed-Type A B
+      ( point-Pointed-Type A , point-Pointed-Type B)
+  inl-glue-smash-prod-Pointed-Type x =
+    ( ap
+      ( map-smash-prod-prod-Pointed-Type A B)
+      ( inv (compute-inl-prod-wedge-Pointed-Type A B x))) ∙
+    ( contraction-map-smash-prod-wedge-Pointed-Type A B
+      ( map-inl-wedge-Pointed-Type A B x))
+
+  inr-glue-smash-prod-Pointed-Type :
+    ( y : type-Pointed-Type B) →
+    map-smash-prod-prod-Pointed-Type A B
+      ( point-Pointed-Type A , y) ＝
+    map-smash-prod-prod-Pointed-Type A B
+      ( point-Pointed-Type A , point-Pointed-Type B)
+  inr-glue-smash-prod-Pointed-Type y =
+    ( ap
+      ( map-smash-prod-prod-Pointed-Type A B)
+      ( inv (compute-inr-prod-wedge-Pointed-Type A B y))) ∙
+    ( contraction-map-smash-prod-wedge-Pointed-Type A B
+      ( map-inr-wedge-Pointed-Type A B y))
+
+  coh-glue-smash-prod-Pointed-Type :
+    inl-glue-smash-prod-Pointed-Type (point-Pointed-Type A) ＝
+    inr-glue-smash-prod-Pointed-Type (point-Pointed-Type B)
+  coh-glue-smash-prod-Pointed-Type =
+    ( identification-left-whisk
+      ( ap
+        ( map-smash-prod-prod-Pointed-Type A B)
+        ( inv (compute-inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
+      ( inv (coh-contraction-map-smash-prod-wedge-Pointed-Type A B))) ∙
+    ( inv
+      ( assoc
+        ( ap (map-smash-prod-prod-Pointed-Type A B)
+          ( inv
+            ( compute-inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
+        ( ap (map-smash-prod-wedge-Pointed-Type A B)
+          ( glue-wedge-Pointed-Type A B))
+        ( contraction-map-smash-prod-wedge-Pointed-Type A B
+          ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))) ∙
+    ( identification-right-whisk
+      ( ( identification-left-whisk
+          ( ap (map-smash-prod-prod-Pointed-Type A B)
+            ( inv
+              ( compute-inl-prod-wedge-Pointed-Type A B
+                ( point-Pointed-Type A))))
+          ( ap-comp
+            ( map-smash-prod-prod-Pointed-Type A B)
+            ( map-prod-wedge-Pointed-Type A B)
+            ( glue-wedge-Pointed-Type A B))) ∙
+        ( inv
+          ( ap-concat
+            ( map-smash-prod-prod-Pointed-Type A B)
+            ( inv
+              ( compute-inl-prod-wedge-Pointed-Type A B
+                ( point-Pointed-Type A)))
+            ( ap
+              ( map-prod-wedge-Pointed-Type A B)
+              ( glue-wedge-Pointed-Type A B)))) ∙
+        ( ap²
+          ( map-smash-prod-prod-Pointed-Type A B)
+          ( inv
+            ( left-transpose-eq-concat
+              ( compute-inl-prod-wedge-Pointed-Type A B
+                ( point-Pointed-Type A))
+              ( inv
+                ( compute-inr-prod-wedge-Pointed-Type A B
+                  ( point-Pointed-Type B)))
+              ( ap
+                ( map-prod-wedge-Pointed-Type A B)
+                ( glue-wedge-Pointed-Type A B))
+              ( inv
+                ( right-transpose-eq-concat
+                  ( ap
+                    ( map-prod-wedge-Pointed-Type A B)
+                    ( glue-wedge-Pointed-Type A B))
+                  ( compute-inr-prod-wedge-Pointed-Type A B
+                    ( point-Pointed-Type B))
+                  ( compute-inl-prod-wedge-Pointed-Type A B
+                    ( point-Pointed-Type A))
+                  ( ( compute-glue-cogap
+                      ( map-pointed-map
+                        ( inclusion-point-Pointed-Type A))
+                      ( map-pointed-map
+                        ( inclusion-point-Pointed-Type B))
+                      ( cocone-type-cocone-Pointed-Type
+                        ( inclusion-point-Pointed-Type A)
+                        ( inclusion-point-Pointed-Type B)
+                        ( cocone-prod-wedge-Pointed-Type A B))
+                      ( point-Pointed-Type unit-Pointed-Type)) ∙
+                    ( right-unit))))))))
+      ( contraction-map-smash-prod-wedge-Pointed-Type A B
+        ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))
+```
+
+### The universal property of the smash product
+
+Fixing a pointed type `B`, the _universal property of the smash product_ states
+that the functor `- ∧∗ B` forms the left-adjoint to the functor `B →∗ -` of
+[pointed maps](structured-types.pointed-maps.md) with source `B`. In the
+language of type theory, this means that we have a pointed equivalence:
+
+```text
+  ((A ∧∗ B) →∗ C) ≃∗ (A →∗ B →∗ C).
+```
+
+**Note:** The categorical product in the category of pointed types is the
+[pointed cartesian product](structured-types.pointed-cartesian-product-types.md).
+
+```agda
+map-universal-property-smash-prod-Pointed-Type :
+  {l1 l2 l3 : Level}
+  (A : Pointed-Type l1) (B : Pointed-Type l2) (C : Pointed-Type l3) →
+  ((A ∧∗ B) →∗ C) → (type-Pointed-Type A) → (B →∗ C)
+pr1 (map-universal-property-smash-prod-Pointed-Type A B C f x) y =
+  map-pointed-map f (map-smash-prod-prod-Pointed-Type A B (x , y))
+pr2 (map-universal-property-smash-prod-Pointed-Type A B C f x) =
+  ( ap
+    ( map-pointed-map f)
+    ( inl-glue-smash-prod-Pointed-Type A B x)) ∙
+  ( preserves-point-pointed-map f)
+
+universal-property-smash-prod-Pointed-Type :
+  {l1 l2 l3 : Level}
+  (A : Pointed-Type l1) (B : Pointed-Type l2) (C : Pointed-Type l3) →
+  ((A ∧∗ B) →∗ C) → (A →∗ (pointed-map-Pointed-Type B C))
+pr1 (universal-property-smash-prod-Pointed-Type A B C f) =
+  map-universal-property-smash-prod-Pointed-Type A B C f
+pr2 (universal-property-smash-prod-Pointed-Type A B C f) =
+  eq-htpy-pointed-Π
+    ( map-universal-property-smash-prod-Pointed-Type A B C
+      ( f)
+      ( point-Pointed-Type A))
+    ( constant-pointed-map B C)
+    ( ( λ y →
+        ( ap
+          ( map-pointed-map f)
+          ( inr-glue-smash-prod-Pointed-Type A B y) ∙
+        ( preserves-point-pointed-map f))) ,
+      ( ( identification-right-whisk
+          ( ap²
+            ( map-pointed-map f)
+            ( inv (coh-glue-smash-prod-Pointed-Type A B)))
+          ( preserves-point-pointed-map f)) ∙
+        ( inv right-unit)))
+```
 
 ## See also
 
diff --git a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
index 1b6c4debfa..b78c57bca8 100644
--- a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.wedges-of-pointed-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
@@ -19,6 +20,7 @@ open import structured-types.pointed-unit-type
 
 open import synthetic-homotopy-theory.cocones-under-spans-of-pointed-types
 open import synthetic-homotopy-theory.cofibers
+open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.pushouts-of-pointed-types
 ```
 
@@ -55,6 +57,32 @@ wedge-Pointed-Type A B =
 infixr 10 _∨∗_
 _∨∗_ = wedge-Pointed-Type
 
+module _
+  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
+  where
+
+  inl-wedge-Pointed-Type : A →∗ (A ∨∗ B)
+  inl-wedge-Pointed-Type =
+    inl-pushout-Pointed-Type
+      ( inclusion-point-Pointed-Type A)
+      ( inclusion-point-Pointed-Type B)
+
+  map-inl-wedge-Pointed-Type :
+    type-Pointed-Type A → type-Pointed-Type (A ∨∗ B)
+  map-inl-wedge-Pointed-Type =
+    map-pointed-map inl-wedge-Pointed-Type
+
+  inr-wedge-Pointed-Type : B →∗ A ∨∗ B
+  inr-wedge-Pointed-Type =
+    inr-pushout-Pointed-Type
+      ( inclusion-point-Pointed-Type A)
+      ( inclusion-point-Pointed-Type B)
+
+  map-inr-wedge-Pointed-Type :
+    type-Pointed-Type B → type-Pointed-Type (A ∨∗ B)
+  map-inr-wedge-Pointed-Type =
+    map-pointed-map inr-wedge-Pointed-Type
+
 indexed-wedge-Pointed-Type :
   {l1 l2 : Level} (I : UU l1) (A : I → Pointed-Type l2) → Pointed-Type (l1 ⊔ l2)
 pr1 (indexed-wedge-Pointed-Type I A) =
@@ -75,11 +103,28 @@ indexed wedge sum, `⋁∗`, is the
 
 ## Properties
 
+### The images of the base points `a : A` and `b : B` are identified in `A ∨∗ B`
+
+```agda
+glue-wedge-Pointed-Type :
+  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
+  map-inl-wedge-Pointed-Type A B (point-Pointed-Type A) ＝
+  map-inr-wedge-Pointed-Type A B (point-Pointed-Type B)
+glue-wedge-Pointed-Type A B =
+  glue-pushout
+    ( map-pointed-map (inclusion-point-Pointed-Type A))
+    ( map-pointed-map (inclusion-point-Pointed-Type B))
+    ( point-Pointed-Type unit-Pointed-Type)
+```
+
 ### The inclusion of the wedge sum `A ∨∗ B` into the pointed product `A ×∗ B`
 
 There is a canonical inclusion of the wedge sum into the pointed product that is
 defined by the cogap map induced by the canonical inclusions `A → A ×∗ B ← B`.
 
+Elements of the form `(x, b)` and `(a, y)`, where `b` and `a` are basepoints,
+lie in the image of the inclusion of the wedge sum into the pointed product.
+
 ```agda
 module _
   {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
@@ -106,6 +151,26 @@ module _
   map-prod-wedge-Pointed-Type :
     type-Pointed-Type (A ∨∗ B) → type-Pointed-Type (A ×∗ B)
   map-prod-wedge-Pointed-Type = pr1 pointed-map-prod-wedge-Pointed-Type
+
+  compute-inl-prod-wedge-Pointed-Type :
+    ( x : type-Pointed-Type A) →
+    ( map-prod-wedge-Pointed-Type (map-inl-wedge-Pointed-Type A B x)) ＝
+    ( x , point-Pointed-Type B)
+  compute-inl-prod-wedge-Pointed-Type =
+    compute-inl-cogap-Pointed-Type
+      ( inclusion-point-Pointed-Type A)
+      ( inclusion-point-Pointed-Type B)
+      ( cocone-prod-wedge-Pointed-Type)
+
+  compute-inr-prod-wedge-Pointed-Type :
+    ( y : type-Pointed-Type B) →
+    ( map-prod-wedge-Pointed-Type (map-inr-wedge-Pointed-Type A B y)) ＝
+    ( point-Pointed-Type A , y)
+  compute-inr-prod-wedge-Pointed-Type =
+    compute-inr-cogap-Pointed-Type
+      ( inclusion-point-Pointed-Type A)
+      ( inclusion-point-Pointed-Type B)
+      ( cocone-prod-wedge-Pointed-Type)
 ```
 
 ## See also