Wedges of pointed types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Victor Blanchi.

Created on 2022-05-13.
Last modified on 2023-09-11.

module synthetic-homotopy-theory.wedges-of-pointed-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import structured-types.pointed-cartesian-product-types
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.cofibers
open import synthetic-homotopy-theory.pushouts-of-pointed-types

Idea

The wedge or wedge sum of two pointed types a : A and b : B is defined by the following pointed pushout:

  unit ------> A
    |          |
    |          |
    v       ⌜  v
    B -----> A ∨∗ B,

and is thus canonically pointed at the identified image of a and b.

Definition

wedge-Pointed-Type :
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
  Pointed-Type (l1 ⊔ l2)
wedge-Pointed-Type A B =
  pushout-Pointed-Type
    ( inclusion-point-Pointed-Type A)
    ( inclusion-point-Pointed-Type B)

infixr 10 _∨∗_
_∨∗_ = 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) =
  cofiber (λ i → (i , point-Pointed-Type (A i)))
pr2 (indexed-wedge-Pointed-Type I A) =
  point-cofiber (λ i → (i , point-Pointed-Type (A i)))

⋁∗ = indexed-wedge-Pointed-Type

Note: the symbols used for the wedge sum _∨∗_ are the logical or ∨ (agda-input: \vee \or) and the asterisk operator ∗ (agda-input: \ast), not the latin small letter v v or the asterisk *. The ⋁ symbol used for the indexed wedge sum, ⋁∗, is the N-ary logical or (agda-input: \bigvee).

Properties

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.

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

  cocone-prod-wedge-Pointed-Type :
    type-cocone-Pointed-Type
      ( inclusion-point-Pointed-Type A)
      ( inclusion-point-Pointed-Type B)
      ( A ×∗ B)
  pr1 cocone-prod-wedge-Pointed-Type = inl-prod-Pointed-Type A B
  pr1 (pr2 cocone-prod-wedge-Pointed-Type) = inr-prod-Pointed-Type A B
  pr1 (pr2 (pr2 cocone-prod-wedge-Pointed-Type)) = refl-htpy
  pr2 (pr2 (pr2 cocone-prod-wedge-Pointed-Type)) = refl

  pointed-map-prod-wedge-Pointed-Type :
    (A ∨∗ B) →∗ (A ×∗ B)
  pointed-map-prod-wedge-Pointed-Type =
    cogap-Pointed-Type
      ( inclusion-point-Pointed-Type A)
      ( inclusion-point-Pointed-Type B)
      ( cocone-prod-wedge-Pointed-Type)

  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

See also

Recent changes