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

Constant span diagrams

module foundation.constant-span-diagrams where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.span-diagrams
open import foundation.spans
open import foundation.universe-levels

open import foundation-core.equivalences

Idea

The constant span diagram at a type X is the span diagram

      id       id
  X <----- X -----> X.

Alternatively, a span diagram

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

is said to be constant if both f and g are equivalences.

Definitions

Constant span diagrams at a type

module _
  {l1 : Level}
  where

  constant-span-diagram : UU l1 → span-diagram l1 l1 l1
  pr1 (constant-span-diagram X) = X
  pr1 (pr2 (constant-span-diagram X)) = X
  pr2 (pr2 (constant-span-diagram X)) = id-span

The predicate of being a constant span diagram

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

  is-constant-span-diagram : UU (l1 ⊔ l2 ⊔ l3)
  is-constant-span-diagram =
    is-equiv (left-map-span-diagram 𝒮) × is-equiv (right-map-span-diagram 𝒮)