# Constant span diagrams

Content created by Egbert Rijke.

Created on 2024-01-28.

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 𝒮)