# Smash products of pointed types

Content created by Fredrik Bakke, Egbert Rijke and maybemabeline.

Created on 2023-05-03.

module synthetic-homotopy-theory.smash-products-of-pointed-types where

Imports
open import foundation.action-on-higher-identifications-functions
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import structured-types.constant-pointed-maps
open import structured-types.pointed-cartesian-product-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-pointed-span-diagrams
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.pushouts-of-pointed-types
open import synthetic-homotopy-theory.wedges-of-pointed-types


## Idea

Given two pointed types a : A and b : B we may form their smash product as the following pushout

 A ∨∗ B ----> A ×∗ B
|           |
|           |
∨         ⌜ ∨
unit -----> A ∧∗ B


where the map A ∨∗ B → A ×∗ B is the canonical inclusion map-wedge-product-Pointed-Type from the wedge into the pointed cartesian product.

## Definition

smash-product-Pointed-Type :
{l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
Pointed-Type (l1 ⊔ l2)
smash-product-Pointed-Type A B =
pushout-Pointed-Type
( pointed-map-product-wedge-Pointed-Type A B)
( terminal-pointed-map (A ∨∗ B))

infixr 15 _∧∗_
_∧∗_ = smash-product-Pointed-Type


Note: The symbols used for the smash product _∧∗_ are the logical and ∧ (agda-input: \wedge \and), and the asterisk operator ∗ (agda-input: \ast), not the asterisk *.

cogap-smash-product-Pointed-Type :
{l1 l2 l3 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {X : Pointed-Type l3} →
cocone-Pointed-Type
( pointed-map-product-wedge-Pointed-Type A B)
( terminal-pointed-map (A ∨∗ B)) X →
(A ∧∗ B) →∗ X
cogap-smash-product-Pointed-Type {A = A} {B} =
cogap-Pointed-Type
( pointed-map-product-wedge-Pointed-Type A B)
( terminal-pointed-map (A ∨∗ B))

map-cogap-smash-product-Pointed-Type :
{l1 l2 l3 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {X : Pointed-Type l3} →
cocone-Pointed-Type
( pointed-map-product-wedge-Pointed-Type A B)
( terminal-pointed-map (A ∨∗ B))
( X) →
type-Pointed-Type (A ∧∗ B) → type-Pointed-Type X
map-cogap-smash-product-Pointed-Type c =
pr1 (cogap-smash-product-Pointed-Type c)


## Properties

### The canonical pointed map from the cartesian product to the smash product

module _
{l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
where

pointed-map-smash-product-product-Pointed-Type : (A ×∗ B) →∗ (A ∧∗ B)
pointed-map-smash-product-product-Pointed-Type =
inl-pushout-Pointed-Type
( pointed-map-product-wedge-Pointed-Type A B)
( terminal-pointed-map (A ∨∗ B))

map-smash-product-product-Pointed-Type :
type-Pointed-Type (A ×∗ B) → type-Pointed-Type (A ∧∗ B)
map-smash-product-product-Pointed-Type =
map-pointed-map pointed-map-smash-product-product-Pointed-Type


### Pointed maps into pointed types A and B induce a pointed map into A ∧∗ B

module _
{l1 l2 l3 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {S : Pointed-Type l3}
where

gap-smash-product-Pointed-Type :
(f : S →∗ A) (g : S →∗ B) → S →∗ (A ∧∗ B)
gap-smash-product-Pointed-Type f g =
pointed-map-smash-product-product-Pointed-Type A B ∘∗
gap-product-Pointed-Type f g

map-gap-smash-product-Pointed-Type :
(f : S →∗ A) (g : S →∗ B) → type-Pointed-Type S → type-Pointed-Type (A ∧∗ B)
map-gap-smash-product-Pointed-Type f g =
pr1 (gap-smash-product-Pointed-Type f g)


### The canonical map from the wedge sum to the smash product identifies all points

module _
{l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
where

pointed-map-smash-product-wedge-Pointed-Type : (A ∨∗ B) →∗ (A ∧∗ B)
pointed-map-smash-product-wedge-Pointed-Type =
pointed-map-smash-product-product-Pointed-Type A B ∘∗
pointed-map-product-wedge-Pointed-Type A B

map-smash-product-wedge-Pointed-Type :
type-Pointed-Type (A ∨∗ B) → type-Pointed-Type (A ∧∗ B)
map-smash-product-wedge-Pointed-Type =
map-pointed-map pointed-map-smash-product-wedge-Pointed-Type

contraction-map-smash-product-wedge-Pointed-Type :
( x : type-Pointed-Type (A ∨∗ B)) →
map-smash-product-wedge-Pointed-Type x ＝
point-Pointed-Type (A ∧∗ B)
contraction-map-smash-product-wedge-Pointed-Type x =
( glue-pushout
( map-product-wedge-Pointed-Type A B)
( map-pointed-map {A = A ∨∗ B} {B = unit-Pointed-Type}
( terminal-pointed-map (A ∨∗ B)))
( x)) ∙
( right-whisker-comp
( htpy-pointed-htpy
( is-initial-unit-Pointed-Type
( A ∧∗ B)
( inr-pushout-Pointed-Type
( pointed-map-product-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-product-wedge-Pointed-Type :
( ap
( map-smash-product-wedge-Pointed-Type)
( glue-wedge-Pointed-Type A B)) ∙
( contraction-map-smash-product-wedge-Pointed-Type
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))) ＝
( contraction-map-smash-product-wedge-Pointed-Type
( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
coh-contraction-map-smash-product-wedge-Pointed-Type =
( map-inv-compute-dependent-identification-eq-value-function
( map-smash-product-wedge-Pointed-Type)
( map-constant-pointed-map (A ∨∗ B) (A ∧∗ B))
( glue-wedge-Pointed-Type A B)
( contraction-map-smash-product-wedge-Pointed-Type
( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
( contraction-map-smash-product-wedge-Pointed-Type
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B)))
( apd
( contraction-map-smash-product-wedge-Pointed-Type)
( glue-wedge-Pointed-Type A B))) ∙
( left-whisker-concat
( contraction-map-smash-product-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.

module _
{l1 l2 : Level}
(A : Pointed-Type l1) (B : Pointed-Type l2)
where

inl-glue-smash-product-Pointed-Type :
( x : type-Pointed-Type A) →
map-smash-product-product-Pointed-Type A B
( x , point-Pointed-Type B) ＝
map-smash-product-product-Pointed-Type A B
( point-Pointed-Type A , point-Pointed-Type B)
inl-glue-smash-product-Pointed-Type x =
( ap
( map-smash-product-product-Pointed-Type A B)
( inv (compute-inl-product-wedge-Pointed-Type A B x))) ∙
( contraction-map-smash-product-wedge-Pointed-Type A B
( map-inl-wedge-Pointed-Type A B x))

inr-glue-smash-product-Pointed-Type :
( y : type-Pointed-Type B) →
map-smash-product-product-Pointed-Type A B
( point-Pointed-Type A , y) ＝
map-smash-product-product-Pointed-Type A B
( point-Pointed-Type A , point-Pointed-Type B)
inr-glue-smash-product-Pointed-Type y =
( ap
( map-smash-product-product-Pointed-Type A B)
( inv (compute-inr-product-wedge-Pointed-Type A B y))) ∙
( contraction-map-smash-product-wedge-Pointed-Type A B
( map-inr-wedge-Pointed-Type A B y))

coh-glue-smash-product-Pointed-Type :
inl-glue-smash-product-Pointed-Type (point-Pointed-Type A) ＝
inr-glue-smash-product-Pointed-Type (point-Pointed-Type B)
coh-glue-smash-product-Pointed-Type =
( left-whisker-concat
( ap
( map-smash-product-product-Pointed-Type A B)
( inv
( compute-inl-product-wedge-Pointed-Type A B (point-Pointed-Type A))))
( inv (coh-contraction-map-smash-product-wedge-Pointed-Type A B))) ∙
( inv
( assoc
( ap (map-smash-product-product-Pointed-Type A B)
( inv
( compute-inl-product-wedge-Pointed-Type A B
( point-Pointed-Type A))))
( ap (map-smash-product-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))
( contraction-map-smash-product-wedge-Pointed-Type A B
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))) ∙
( right-whisker-concat
( ( left-whisker-concat
( ap (map-smash-product-product-Pointed-Type A B)
( inv
( compute-inl-product-wedge-Pointed-Type A B
( point-Pointed-Type A))))
( ap-comp
( map-smash-product-product-Pointed-Type A B)
( map-product-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))) ∙
( inv
( ap-concat
( map-smash-product-product-Pointed-Type A B)
( inv
( compute-inl-product-wedge-Pointed-Type A B
( point-Pointed-Type A)))
( ap
( map-product-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B)))) ∙
( ap²
( map-smash-product-product-Pointed-Type A B)
( inv
( left-transpose-eq-concat
( compute-inl-product-wedge-Pointed-Type A B
( point-Pointed-Type A))
( inv
( compute-inr-product-wedge-Pointed-Type A B
( point-Pointed-Type B)))
( ap
( map-product-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))
( inv
( right-transpose-eq-concat
( ap
( map-product-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))
( compute-inr-product-wedge-Pointed-Type A B
( point-Pointed-Type B))
( compute-inl-product-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-cocone-Pointed-Type
( inclusion-point-Pointed-Type A)
( inclusion-point-Pointed-Type B)
( cocone-product-wedge-Pointed-Type A B))
( point-Pointed-Type unit-Pointed-Type)) ∙
( right-unit))))))))
( contraction-map-smash-product-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 with source B. In the language of type theory, this means that we have a pointed equivalence:

  ((A ∧∗ B) →∗ C) ≃∗ (A →∗ B →∗ C).


Note: The categorical product in the category of pointed types is the pointed cartesian product.

module _
{l1 l2 l3 : Level}
(A : Pointed-Type l1) (B : Pointed-Type l2) (C : Pointed-Type l3)
(f : (A ∧∗ B) →∗ C)
where

map-map-universal-property-smash-product-Pointed-Type :
type-Pointed-Type A → type-Pointed-Type B → type-Pointed-Type C
map-map-universal-property-smash-product-Pointed-Type x y =
map-pointed-map f (map-smash-product-product-Pointed-Type A B (x , y))

preserves-point-map-map-universal-property-smash-product-Pointed-Type :
(x : type-Pointed-Type A) →
map-map-universal-property-smash-product-Pointed-Type x
( point-Pointed-Type B) ＝
point-Pointed-Type C
preserves-point-map-map-universal-property-smash-product-Pointed-Type x =
( ap
( map-pointed-map f)
( inl-glue-smash-product-Pointed-Type A B x)) ∙
( preserves-point-pointed-map f)

map-universal-property-smash-product-Pointed-Type :
type-Pointed-Type A → (B →∗ C)
pr1 (map-universal-property-smash-product-Pointed-Type x) =
map-map-universal-property-smash-product-Pointed-Type x
pr2 (map-universal-property-smash-product-Pointed-Type x) =
preserves-point-map-map-universal-property-smash-product-Pointed-Type x

htpy-preserves-point-map-universal-property-smash-product-Pointed-Type :
map-map-universal-property-smash-product-Pointed-Type
( point-Pointed-Type A) ~
map-constant-pointed-map B C
htpy-preserves-point-map-universal-property-smash-product-Pointed-Type y =
( ap (map-pointed-map f) (inr-glue-smash-product-Pointed-Type A B y)) ∙
( preserves-point-pointed-map f)

coherence-point-preserves-point-map-universal-property-smash-product-Pointed-Type :
coherence-point-unpointed-htpy-pointed-Π
( map-universal-property-smash-product-Pointed-Type
( point-Pointed-Type A))
( constant-pointed-map B C)
( htpy-preserves-point-map-universal-property-smash-product-Pointed-Type)
coherence-point-preserves-point-map-universal-property-smash-product-Pointed-Type =
( right-whisker-concat
( ap²
( map-pointed-map f)
( coh-glue-smash-product-Pointed-Type A B))
( preserves-point-pointed-map f)) ∙
( inv right-unit)

pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type :
map-universal-property-smash-product-Pointed-Type (point-Pointed-Type A) ~∗
constant-pointed-map B C
pr1
pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type =
htpy-preserves-point-map-universal-property-smash-product-Pointed-Type
pr2
pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type =
coherence-point-preserves-point-map-universal-property-smash-product-Pointed-Type

preserves-point-map-universal-property-smash-product-Pointed-Type :
map-universal-property-smash-product-Pointed-Type (point-Pointed-Type A) ＝
constant-pointed-map B C
preserves-point-map-universal-property-smash-product-Pointed-Type =
eq-pointed-htpy
( map-universal-property-smash-product-Pointed-Type
( point-Pointed-Type A))
( constant-pointed-map B C)
( pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type)

pointed-map-universal-property-smash-product-Pointed-Type :
A →∗ (pointed-map-Pointed-Type B C)
pr1 pointed-map-universal-property-smash-product-Pointed-Type =
map-universal-property-smash-product-Pointed-Type
pr2 pointed-map-universal-property-smash-product-Pointed-Type =
preserves-point-map-universal-property-smash-product-Pointed-Type