Species of finite inhabited types

module species.species-of-finite-inhabited-types where

open import foundation.universe-levels

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

open import univalent-combinatorics.finite-types
open import univalent-combinatorics.inhabited-finite-types

Idea

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

Definition

species-Inhabited-𝔽 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
species-Inhabited-𝔽 l1 l2 =
  species-subuniverse (is-finite-and-inhabited-Prop {l1}) (is-finite-Prop {l2})