Terminal spans on families of types

Content created by Egbert Rijke.

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

module foundation.terminal-spans-families-of-types where
Imports 
open import foundation.contractible-types
open import foundation.morphisms-spans-families-of-types
open import foundation.spans-families-of-types
open import foundation.universe-levels

Idea

A span 𝒮 on a family of types A : I → 𝒰 is said to be terminal if for each span 𝒯 on A the type of morphisms of spans 𝒯 → 𝒮 is contractible.

Definitions

The predicate of being a terminal span on a family of types

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

  is-terminal-span-type-family : UUω
  is-terminal-span-type-family =
    {l : Level} (𝒯 : span-type-family l A) →
    is-contr (hom-span-type-family 𝒯 𝒮)

See also

Recent changes