Span diagrams on families of types

Content created by Egbert Rijke.

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

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


A span diagram on a family of types indexed by a type I consists of a type family A : I → 𝒰, and a span on the type family A. More explicitly, a span diagram on a family of types indexed by I consists of a type family A : I → 𝒰, a spanning type S, and a family of maps f : (i : I) → S → A i.


Span diagrams of families of types

span-diagram-type-family :
  {l1 : Level} (l2 l3 : Level)  UU l1  UU (l1  lsuc l2  lsuc l3)
span-diagram-type-family l2 l3 I =
  Σ (I  UU l2)  A  span-type-family l3 A)

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

  family-span-diagram-type-family : I  UU l2
  family-span-diagram-type-family = pr1 s

  span-span-diagram-type-family :
    span-type-family l3 family-span-diagram-type-family
  span-span-diagram-type-family = pr2 s

  spanning-type-span-diagram-type-family : UU l3
  spanning-type-span-diagram-type-family =
      ( span-span-diagram-type-family)

  map-span-diagram-type-family :
    (i : I)  spanning-type-span-diagram-type-family 
    family-span-diagram-type-family i
  map-span-diagram-type-family =
      ( span-span-diagram-type-family)

Recent changes