Diagonal span diagrams

Content created by Egbert Rijke.

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

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

Recent changes