Species

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

Created on 2023-03-21.
Last modified on 2024-09-23.

Modules in the species namespace

module species where

open import species.cartesian-exponents-species-of-types public
open import species.cartesian-products-species-of-types public
open import species.cauchy-composition-species-of-types public
open import species.cauchy-composition-species-of-types-in-subuniverses public
open import species.cauchy-exponentials-species-of-types public
open import species.cauchy-exponentials-species-of-types-in-subuniverses public
open import species.cauchy-products-species-of-types public
open import species.cauchy-products-species-of-types-in-subuniverses public
open import species.cauchy-series-species-of-types public
open import species.cauchy-series-species-of-types-in-subuniverses public
open import species.composition-cauchy-series-species-of-types public
open import species.composition-cauchy-series-species-of-types-in-subuniverses public
open import species.coproducts-species-of-types public
open import species.coproducts-species-of-types-in-subuniverses public
open import species.cycle-index-series-species-of-types public
open import species.derivatives-species-of-types public
open import species.dirichlet-exponentials-species-of-types public
open import species.dirichlet-exponentials-species-of-types-in-subuniverses public
open import species.dirichlet-products-species-of-types public
open import species.dirichlet-products-species-of-types-in-subuniverses public
open import species.dirichlet-series-species-of-finite-inhabited-types public
open import species.dirichlet-series-species-of-types public
open import species.dirichlet-series-species-of-types-in-subuniverses public
open import species.equivalences-species-of-types public
open import species.equivalences-species-of-types-in-subuniverses public
open import species.exponentials-cauchy-series-of-types public
open import species.exponentials-cauchy-series-of-types-in-subuniverses public
open import species.hasse-weil-species public
open import species.morphisms-finite-species public
open import species.morphisms-species-of-types public
open import species.pointing-species-of-types public
open import species.precategory-of-finite-species public
open import species.products-cauchy-series-species-of-types public
open import species.products-cauchy-series-species-of-types-in-subuniverses public
open import species.products-dirichlet-series-species-of-finite-inhabited-types public
open import species.products-dirichlet-series-species-of-types public
open import species.products-dirichlet-series-species-of-types-in-subuniverses public
open import species.small-cauchy-composition-species-of-finite-inhabited-types public
open import species.small-cauchy-composition-species-of-types-in-subuniverses public
open import species.species-of-finite-inhabited-types public
open import species.species-of-finite-types public
open import species.species-of-inhabited-types public
open import species.species-of-types public
open import species.species-of-types-in-subuniverses public
open import species.unit-cauchy-composition-species-of-types public
open import species.unit-cauchy-composition-species-of-types-in-subuniverses public
open import species.unlabeled-structures-species public

Recent changes

• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2023-06-08. Victor Blanchi, Fredrik Bakke and Egbert Rijke. Product of Dirichlet series (#643).
• 2023-05-25. Victor Blanchi and Egbert Rijke. Towards Hasse-Weil species (#631).
• 2023-05-25. Victor Blanchi and Egbert Rijke. Dirichlet exponential of species (of types and of types in a subuniverse) (#628).
• 2023-05-22. Victor Blanchi and Fredrik Bakke. Definition of dirichlet series (#626).