# Operations on span diagrams

Content created by Egbert Rijke.

Created on 2024-01-28.

module foundation-core.operations-span-diagrams where

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

open import foundation-core.function-types


## Idea

This file contains some operations on span diagrams that produce new span diagrams from given span diagrams and possibly other data.

## Definitions

### Concatenating span diagrams and maps on both sides

Consider a span diagram 𝒮 given by

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


and maps i : A → A' and j : B → B'. The concatenation-span-diagram of 𝒮, i, and j is the span diagram

       i ∘ f     j ∘ g
A' <------- S -------> B'.

module _
{l1 l2 l3 l4 l5 : Level}
where

concat-span-diagram :
(𝒮 : span-diagram l1 l2 l3)
{A' : UU l4} (f : domain-span-diagram 𝒮 → A')
{B' : UU l5} (g : codomain-span-diagram 𝒮 → B') →
span-diagram l4 l5 l3
pr1 (concat-span-diagram 𝒮 {A'} f {B'} g) =
A'
pr1 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) =
B'
pr2 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) =
concat-span (span-span-diagram 𝒮) f g


### Concatenating span diagrams and maps on the left

Consider a span diagram 𝒮 given by

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


and a map i : A → A'. The left concatenation of 𝒮 and i is the span diagram

       i ∘ f      g
A' <------- S -----> B.

module _
{l1 l2 l3 l4 : Level}
where

left-concat-span-diagram :
(𝒮 : span-diagram l1 l2 l3) {A' : UU l4} →
(domain-span-diagram 𝒮 → A') → span-diagram l4 l2 l3
left-concat-span-diagram 𝒮 f = concat-span-diagram 𝒮 f id


### Concatenating span diagrams and maps on the right

Consider a span diagram 𝒮 given by

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


and a map j : B → B'. The right concatenation of 𝒮 by j is the span diagram

        f      j ∘ g
A' <----- S -------> B'.

module _
{l1 l2 l3 l4 : Level}
where

right-concat-span-diagram :
(𝒮 : span-diagram l1 l2 l3) {B' : UU l4} →
(codomain-span-diagram 𝒮 → B') → span-diagram l1 l4 l3
right-concat-span-diagram 𝒮 g = concat-span-diagram 𝒮 id g


### Concatenation of span diagrams and morphisms of arrows on the left

Consider a span diagram 𝒮 given by

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


and a morphism of arrows h : hom-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 : hom-arrow f' (left-map-span-diagram 𝒮))
where

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

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

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

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

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

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

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


### Concatenation of span diagrams and morphisms of arrows on the right

Consider a span diagram 𝒮 given by

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


and a morphism of arrows h : hom-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 : hom-arrow g' (right-map-span-diagram 𝒮))
where

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

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

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

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

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

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

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