Left half-smash products

Content created by Fredrik Bakke.

Created on 2025-02-14.
Last modified on 2025-02-14.

module synthetic-homotopy-theory.left-half-smash-products where

Imports

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-types

open import synthetic-homotopy-theory.cofibers-of-maps

Idea

Given a type A and a pointed type b : B we may form the left half-smash product^¶ A ⋉∗ B as the cofiber of the canonical inclusion A → A × B at the base point of B. In other words, the left half-smash product is the pushout

    A  -----> A × B
    |           |
    |           |
    ∨         ⌜ ∨
    * ------> A ⋉∗ B.

Definitions

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

  map-left-half-smash : A → A × type-Pointed-Type B
  map-left-half-smash a = (a , point-Pointed-Type B)

  type-left-half-smash : UU (l1 ⊔ l2)
  type-left-half-smash =
    cofiber map-left-half-smash

  point-left-half-smash : type-left-half-smash
  point-left-half-smash =
    point-cofiber map-left-half-smash

  pointed-type-left-half-smash : Pointed-Type (l1 ⊔ l2)
  pointed-type-left-half-smash =
    pointed-type-cofiber map-left-half-smash

  infixr 15 _⋉∗_
  _⋉∗_ : Pointed-Type (l1 ⊔ l2)
  _⋉∗_ = pointed-type-left-half-smash

Notation. The symbols used for the left half-smash product _⋉∗_ are the left normal factor semidirect product ⋉ (agda-input: \ltimes \join), and the asterisk operator ∗ (agda-input: \ast), not the asterisk *.