This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Diagonal span diagrams

module foundation.diagonal-span-diagrams where
Imports 
open import foundation.span-diagrams
open import foundation.universe-levels

Idea

Consider a map f : A → B. The diagonal span diagram of f is the span diagram

       f       f
  B <----- A -----> B.

Definitions

Diagonal span diagrams of maps

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  where

  diagonal-span-diagram : span-diagram l2 l2 l1
  diagonal-span-diagram = make-span-diagram f f