Species of inhabited types

Content created by Egbert Rijke and Victor Blanchi.

Created on 2023-03-21.
Last modified on 2023-04-27.

module species.species-of-inhabited-types where
Imports 
open import foundation.inhabited-types
open import foundation.unit-type
open import foundation.universe-levels

open import species.species-of-types-in-subuniverses

Idea

A species of inhabited types is a map from the subuniverse of inhabited types to a universe.

Definition

species-inhabited-types : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
species-inhabited-types l1 l2 =
  species-subuniverse (is-inhabited-Prop {l1}) λ (X : UU l2) → unit-Prop

Recent changes