Pointed span diagrams

Content created by Egbert Rijke.

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

module structured-types.pointed-span-diagrams where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.morphisms-arrows
open import foundation.universe-levels

open import structured-types.morphisms-pointed-arrows
open import structured-types.pointed-maps
open import structured-types.pointed-spans
open import structured-types.pointed-types

Idea

A (binary) pointed span diagram is a diagram of pointed maps of the form

       f       g
  A <----- S -----> B.

In other words, a pointed span diagram consists of two pointed types A and B and a pointed span from A to B.

(Binary) span diagrams of pointed types

pointed-span-diagram :
  (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
pointed-span-diagram l1 l2 l3 =
  Σ ( Pointed-Type l1)
    ( λ A → Σ (Pointed-Type l2) (pointed-span l3 A))

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

  make-pointed-span-diagram :
    (S →∗ A) → (S →∗ B) → pointed-span-diagram l2 l3 l1
  make-pointed-span-diagram f g = (A , B , S , f , g)

module _
  {l1 l2 l3 : Level} (𝒮 : pointed-span-diagram l1 l2 l3)
  where

  pointed-domain-pointed-span-diagram : Pointed-Type l1
  pointed-domain-pointed-span-diagram = pr1 𝒮

  domain-pointed-span-diagram : UU l1
  domain-pointed-span-diagram =
    type-Pointed-Type pointed-domain-pointed-span-diagram

  point-domain-pointed-span-diagram :
    domain-pointed-span-diagram
  point-domain-pointed-span-diagram =
    point-Pointed-Type pointed-domain-pointed-span-diagram

  pointed-codomain-pointed-span-diagram : Pointed-Type l2
  pointed-codomain-pointed-span-diagram = pr1 (pr2 𝒮)

  codomain-pointed-span-diagram : UU l2
  codomain-pointed-span-diagram =
    type-Pointed-Type pointed-codomain-pointed-span-diagram

  point-codomain-pointed-span-diagram :
    codomain-pointed-span-diagram
  point-codomain-pointed-span-diagram =
    point-Pointed-Type pointed-codomain-pointed-span-diagram

  pointed-span-pointed-span-diagram :
    pointed-span l3
      ( pointed-domain-pointed-span-diagram)
      ( pointed-codomain-pointed-span-diagram)
  pointed-span-pointed-span-diagram = pr2 (pr2 𝒮)

  spanning-pointed-type-pointed-span-diagram : Pointed-Type l3
  spanning-pointed-type-pointed-span-diagram =
    spanning-pointed-type-pointed-span
      ( pointed-span-pointed-span-diagram)

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

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

  left-pointed-map-pointed-span-diagram :
    spanning-pointed-type-pointed-span-diagram →∗
    pointed-domain-pointed-span-diagram
  left-pointed-map-pointed-span-diagram =
    left-pointed-map-pointed-span
      ( pointed-span-pointed-span-diagram)

  left-map-pointed-span-diagram :
    spanning-type-pointed-span-diagram → domain-pointed-span-diagram
  left-map-pointed-span-diagram =
    left-map-pointed-span
      ( pointed-span-pointed-span-diagram)

  preserves-point-left-map-pointed-span-diagram :
    left-map-pointed-span-diagram
      ( point-spanning-type-pointed-span-diagram) ＝
    point-domain-pointed-span-diagram
  preserves-point-left-map-pointed-span-diagram =
    preserves-point-left-map-pointed-span
      ( pointed-span-pointed-span-diagram)

  right-pointed-map-pointed-span-diagram :
    spanning-pointed-type-pointed-span-diagram →∗
    pointed-codomain-pointed-span-diagram
  right-pointed-map-pointed-span-diagram =
    right-pointed-map-pointed-span
      ( pointed-span-pointed-span-diagram)

  right-map-pointed-span-diagram :
    spanning-type-pointed-span-diagram → codomain-pointed-span-diagram
  right-map-pointed-span-diagram =
    right-map-pointed-span
      ( pointed-span-pointed-span-diagram)

  preserves-point-right-map-pointed-span-diagram :
    right-map-pointed-span-diagram
      ( point-spanning-type-pointed-span-diagram) ＝
    point-codomain-pointed-span-diagram
  preserves-point-right-map-pointed-span-diagram =
    preserves-point-right-map-pointed-span
      ( pointed-span-pointed-span-diagram)

The pointed span diagram obtained from a morphism of pointed arrows

Given pointed maps f : A →∗ B and g : X →∗ Y and a morphism of pointed arrows α : f →∗ g, the pointed span diagram associated to α is the pointed span diagram

       f       α₀
  B <----- A -----> X.

module _
  {l1 l2 l3 l4 : Level}
  {A : Pointed-Type l1} {B : Pointed-Type l2}
  {X : Pointed-Type l3} {Y : Pointed-Type l4}
  (f : A →∗ B) (g : X →∗ Y) (α : hom-pointed-arrow f g)
  where

  domain-span-diagram-hom-pointed-arrow : Pointed-Type l2
  domain-span-diagram-hom-pointed-arrow = B

  type-domain-span-diagram-hom-pointed-arrow : UU l2
  type-domain-span-diagram-hom-pointed-arrow =
    type-Pointed-Type domain-span-diagram-hom-pointed-arrow

  point-domain-span-diagram-hom-pointed-arrow :
    type-domain-span-diagram-hom-pointed-arrow
  point-domain-span-diagram-hom-pointed-arrow =
    point-Pointed-Type domain-span-diagram-hom-pointed-arrow

  codomain-span-diagram-hom-pointed-arrow : Pointed-Type l3
  codomain-span-diagram-hom-pointed-arrow = X

  type-codomain-span-diagram-hom-pointed-arrow : UU l3
  type-codomain-span-diagram-hom-pointed-arrow =
    type-Pointed-Type codomain-span-diagram-hom-pointed-arrow

  point-codomain-span-diagram-hom-pointed-arrow :
    type-codomain-span-diagram-hom-pointed-arrow
  point-codomain-span-diagram-hom-pointed-arrow =
    point-Pointed-Type codomain-span-diagram-hom-pointed-arrow

  pointed-spanning-type-hom-pointed-arrow : Pointed-Type l1
  pointed-spanning-type-hom-pointed-arrow = A

  spanning-type-hom-pointed-arrow : UU l1
  spanning-type-hom-pointed-arrow =
    type-Pointed-Type pointed-spanning-type-hom-pointed-arrow

  point-spanning-type-hom-pointed-arrow :
    spanning-type-hom-pointed-arrow
  point-spanning-type-hom-pointed-arrow =
    point-Pointed-Type pointed-spanning-type-hom-pointed-arrow

  left-pointed-map-span-diagram-hom-pointed-arrow :
    pointed-spanning-type-hom-pointed-arrow →∗
    domain-span-diagram-hom-pointed-arrow
  left-pointed-map-span-diagram-hom-pointed-arrow = f

  left-map-span-diagram-hom-pointed-arrow :
    spanning-type-hom-pointed-arrow → type-domain-span-diagram-hom-pointed-arrow
  left-map-span-diagram-hom-pointed-arrow =
    map-pointed-map left-pointed-map-span-diagram-hom-pointed-arrow

  preserves-point-left-map-span-diagram-hom-pointed-arrow :
    left-map-span-diagram-hom-pointed-arrow
      ( point-spanning-type-hom-pointed-arrow) ＝
    point-domain-span-diagram-hom-pointed-arrow
  preserves-point-left-map-span-diagram-hom-pointed-arrow =
    preserves-point-pointed-map
      ( left-pointed-map-span-diagram-hom-pointed-arrow)

  right-pointed-map-span-diagram-hom-pointed-arrow :
    pointed-spanning-type-hom-pointed-arrow →∗
    codomain-span-diagram-hom-pointed-arrow
  right-pointed-map-span-diagram-hom-pointed-arrow =
    pointed-map-domain-hom-pointed-arrow f g α

  right-map-span-diagram-hom-pointed-arrow :
    spanning-type-hom-pointed-arrow →
    type-codomain-span-diagram-hom-pointed-arrow
  right-map-span-diagram-hom-pointed-arrow =
    map-pointed-map right-pointed-map-span-diagram-hom-pointed-arrow

  preserves-point-right-map-span-diagram-hom-pointed-arrow :
    right-map-span-diagram-hom-pointed-arrow
      ( point-spanning-type-hom-pointed-arrow) ＝
    point-codomain-span-diagram-hom-pointed-arrow
  preserves-point-right-map-span-diagram-hom-pointed-arrow =
    preserves-point-pointed-map
      ( right-pointed-map-span-diagram-hom-pointed-arrow)

  span-hom-pointed-arrow :
    pointed-span l1 B X
  pr1 span-hom-pointed-arrow =
    A
  pr1 (pr2 span-hom-pointed-arrow) =
    left-pointed-map-span-diagram-hom-pointed-arrow
  pr2 (pr2 span-hom-pointed-arrow) =
    right-pointed-map-span-diagram-hom-pointed-arrow

  span-diagram-hom-pointed-arrow : pointed-span-diagram l2 l3 l1
  pr1 span-diagram-hom-pointed-arrow =
    domain-span-diagram-hom-pointed-arrow
  pr1 (pr2 span-diagram-hom-pointed-arrow) =
    codomain-span-diagram-hom-pointed-arrow
  pr2 (pr2 span-diagram-hom-pointed-arrow) =
    span-hom-pointed-arrow

See also

Recent changes