Operations on span diagrams

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-04-25.

module foundation.operations-span-diagrams where

open import foundation-core.operations-span-diagrams public
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences-arrows
open import foundation.operations-spans
open import foundation.span-diagrams
open import foundation.spans
open import foundation.universe-levels

Idea

This file contains some further operations on span diagrams that produce new span diagrams from given span diagrams and possibly other data. Previous operations on span diagrams were defined in foundation-core.operations-span-diagrams.

Definitions

Concatenating span diagrams and equivalences of arrows on the left

Consider a span diagram 𝒮 given by

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

and an equivalence of arrows h : equiv-arrow f' f as indicated in the diagram

          f'
     A' <---- S'
     |        |
  h₀ | ≃    ≃ | h₁
     ∨        ∨
     A <----- S -----> B.
          f       g

Then we obtain a span diagram A' <- S' -> B.

module _
  {l1 l2 l3 l4 l5 : Level} (𝒮 : span-diagram l1 l2 l3)
  {S' : UU l4} {A' : UU l5} (f' : S' → A')
  (h : equiv-arrow f' (left-map-span-diagram 𝒮))
  where

  domain-left-concat-equiv-arrow-span-diagram : UU l5
  domain-left-concat-equiv-arrow-span-diagram = A'

  codomain-left-concat-equiv-arrow-span-diagram : UU l2
  codomain-left-concat-equiv-arrow-span-diagram = codomain-span-diagram 𝒮

  span-left-concat-equiv-arrow-span-diagram :
    span l4
      ( domain-left-concat-equiv-arrow-span-diagram)
      ( codomain-left-concat-equiv-arrow-span-diagram)
  span-left-concat-equiv-arrow-span-diagram =
    left-concat-equiv-arrow-span (span-span-diagram 𝒮) f' h

  left-concat-equiv-arrow-span-diagram : span-diagram l5 l2 l4
  pr1 left-concat-equiv-arrow-span-diagram =
    domain-left-concat-equiv-arrow-span-diagram
  pr1 (pr2 left-concat-equiv-arrow-span-diagram) =
    codomain-left-concat-equiv-arrow-span-diagram
  pr2 (pr2 left-concat-equiv-arrow-span-diagram) =
    span-left-concat-equiv-arrow-span-diagram

  spanning-type-left-concat-equiv-arrow-span-diagram : UU l4
  spanning-type-left-concat-equiv-arrow-span-diagram =
    spanning-type-span-diagram left-concat-equiv-arrow-span-diagram

  left-map-left-concat-equiv-arrow-span-diagram :
    spanning-type-left-concat-equiv-arrow-span-diagram →
    domain-left-concat-equiv-arrow-span-diagram
  left-map-left-concat-equiv-arrow-span-diagram =
    left-map-span-diagram left-concat-equiv-arrow-span-diagram

  right-map-left-concat-equiv-arrow-span-diagram :
    spanning-type-left-concat-equiv-arrow-span-diagram →
    codomain-left-concat-equiv-arrow-span-diagram
  right-map-left-concat-equiv-arrow-span-diagram =
    right-map-span-diagram left-concat-equiv-arrow-span-diagram

Concatenating span diagrams and equivalences of arrows on the right

Consider a span diagram 𝒮 given by

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

and a equivalence of arrows h : equiv-arrow g' g as indicated in the diagram

               g'
           S' ----> B'
           |        |
        h₀ | ≃    ≃ | h₁
           ∨        ∨
  A <----- S -----> B.
       f       g

Then we obtain a span diagram A <- S' -> B'.

module _
  {l1 l2 l3 l4 l5 : Level} (𝒮 : span-diagram l1 l2 l3)
  {S' : UU l4} {B' : UU l5} (g' : S' → B')
  (h : equiv-arrow g' (right-map-span-diagram 𝒮))
  where

  domain-right-concat-equiv-arrow-span-diagram : UU l1
  domain-right-concat-equiv-arrow-span-diagram = domain-span-diagram 𝒮

  codomain-right-concat-equiv-arrow-span-diagram : UU l5
  codomain-right-concat-equiv-arrow-span-diagram = B'

  span-right-concat-equiv-arrow-span-diagram :
    span l4
      ( domain-right-concat-equiv-arrow-span-diagram)
      ( codomain-right-concat-equiv-arrow-span-diagram)
  span-right-concat-equiv-arrow-span-diagram =
    right-concat-equiv-arrow-span (span-span-diagram 𝒮) g' h

  right-concat-equiv-arrow-span-diagram : span-diagram l1 l5 l4
  pr1 right-concat-equiv-arrow-span-diagram =
    domain-right-concat-equiv-arrow-span-diagram
  pr1 (pr2 right-concat-equiv-arrow-span-diagram) =
    codomain-right-concat-equiv-arrow-span-diagram
  pr2 (pr2 right-concat-equiv-arrow-span-diagram) =
    span-right-concat-equiv-arrow-span-diagram

  spanning-type-right-concat-equiv-arrow-span-diagram : UU l4
  spanning-type-right-concat-equiv-arrow-span-diagram =
    spanning-type-span-diagram right-concat-equiv-arrow-span-diagram

  left-map-right-concat-equiv-arrow-span-diagram :
    spanning-type-right-concat-equiv-arrow-span-diagram →
    domain-right-concat-equiv-arrow-span-diagram
  left-map-right-concat-equiv-arrow-span-diagram =
    left-map-span-diagram right-concat-equiv-arrow-span-diagram

  right-map-right-concat-equiv-arrow-span-diagram :
    spanning-type-right-concat-equiv-arrow-span-diagram →
    codomain-right-concat-equiv-arrow-span-diagram
  right-map-right-concat-equiv-arrow-span-diagram =
    right-map-span-diagram right-concat-equiv-arrow-span-diagram

Recent changes