Pointed spans

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-03-13.

module structured-types.pointed-spans where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.spans
open import foundation.universe-levels

open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

Consider two pointed types A and B. A (binary) pointed span from A to B consists of a spanning pointed type S and a pair of pointed maps f : S →∗ A and g : S →∗ B. The pointed types A and B in the specification of a binary span of pointed types are also referred to as the domain and codomain of the pointed span, respectively.

Definitions

(Binary) pointed spans

pointed-span :
  {l1 l2 : Level} (l : Level) (A : Pointed-Type l1) (B : Pointed-Type l2) →
  UU (l1 ⊔ l2 ⊔ lsuc l)
pointed-span l A B = Σ (Pointed-Type l) (λ S → (S →∗ A) × (S →∗ B))

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

  spanning-pointed-type-pointed-span : Pointed-Type l3
  spanning-pointed-type-pointed-span = pr1 𝒮

  spanning-type-pointed-span : UU l3
  spanning-type-pointed-span =
    type-Pointed-Type spanning-pointed-type-pointed-span

  point-spanning-type-pointed-span : spanning-type-pointed-span
  point-spanning-type-pointed-span =
    point-Pointed-Type spanning-pointed-type-pointed-span

  left-pointed-map-pointed-span :
    spanning-pointed-type-pointed-span →∗ A
  left-pointed-map-pointed-span = pr1 (pr2 𝒮)

  left-map-pointed-span :
    spanning-type-pointed-span → type-Pointed-Type A
  left-map-pointed-span =
    map-pointed-map left-pointed-map-pointed-span

  preserves-point-left-map-pointed-span :
    left-map-pointed-span point-spanning-type-pointed-span ＝
    point-Pointed-Type A
  preserves-point-left-map-pointed-span =
    preserves-point-pointed-map left-pointed-map-pointed-span

  right-pointed-map-pointed-span :
    spanning-pointed-type-pointed-span →∗ B
  right-pointed-map-pointed-span = pr2 (pr2 𝒮)

  right-map-pointed-span :
    spanning-type-pointed-span → type-Pointed-Type B
  right-map-pointed-span =
    map-pointed-map right-pointed-map-pointed-span

  preserves-point-right-map-pointed-span :
    right-map-pointed-span point-spanning-type-pointed-span ＝
    point-Pointed-Type B
  preserves-point-right-map-pointed-span =
    preserves-point-pointed-map right-pointed-map-pointed-span

  span-pointed-span : span l3 (type-Pointed-Type A) (type-Pointed-Type B)
  pr1 span-pointed-span = spanning-type-pointed-span
  pr1 (pr2 span-pointed-span) = left-map-pointed-span
  pr2 (pr2 span-pointed-span) = right-map-pointed-span

Identity pointed spans

module _
  {l1 : Level} {X : Pointed-Type l1}
  where

  id-pointed-span : pointed-span l1 X X
  pr1 id-pointed-span = X
  pr1 (pr2 id-pointed-span) = id-pointed-map
  pr2 (pr2 id-pointed-span) = id-pointed-map

See also

Recent changes