Spans of families of types

Content created by Egbert Rijke.

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

module foundation.spans-families-of-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types

Idea

Consider a family of types A i indexed by i : I. A span on A consists of a type S equipped with a family of maps

  (i : I) → S → A i.

The type S is called the spanning type of the span.

Definitions

Spans on families of types

module _
  {l1 l2 : Level} (l3 : Level) {I : UU l1} (A : I → UU l2)
  where

  span-type-family : UU (l1 ⊔ l2 ⊔ lsuc l3)
  span-type-family = Σ (UU l3) (λ S → (i : I) → S → A i)

module _
  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2}
  (s : span-type-family l3 A)
  where

  spanning-type-span-type-family : UU l3
  spanning-type-span-type-family = pr1 s

  map-span-type-family :
    (i : I) → spanning-type-span-type-family → A i
  map-span-type-family = pr2 s

See also

Recent changes