Species of finite types

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-03-21.
Last modified on 2025-02-11.

module species.species-of-finite-types where
Imports 
open import foundation.universe-levels

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

open import univalent-combinatorics.finite-types

Idea

A species of finite types is a map from Finite-Type to a Finite-Type.

Definition

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

Recent changes