The unit of Cauchy composition of types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-27.
Last modified on 2023-05-16.

module species.unit-cauchy-composition-species-of-types where
Imports 
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

Recent changes