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

The unit of Cauchy composition of types

module species.unit-cauchy-composition-species-of-types where

open import foundation.contractible-types
open import foundation.universe-levels

open import species.species-of-types

Idea

The unit of Cauchy composition of species of types is the species

  X ↦ is-contr X.

Definition

unit-species-types : {l1 : Level} → species-types l1 l1
unit-species-types = is-contr