This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The precategory of finite species

module species.precategory-of-finite-species where
Imports 
open import category-theory.large-precategories

open import foundation.universe-levels

open import species.morphisms-finite-species
open import species.species-of-finite-types

Idea

The precategory of finite species consists of finite species and homomorphisms of finite species.

Definition

species-𝔽-Large-Precategory :
  (l : Level) →
  Large-Precategory (λ l1 → lsuc l ⊔ lsuc l1) (λ l2 l3 → lsuc l ⊔ l2 ⊔ l3)
species-𝔽-Large-Precategory l =
  make-Large-Precategory
    ( species-𝔽 l)
    ( hom-set-species-𝔽)
    ( λ {l1} {l2} {l3} {F} {G} {H} → comp-hom-species-𝔽 F G H)
    ( λ {l1} {F} → id-hom-species-𝔽 F)
    ( λ {l1} {l2} {l3} {l4} {F} {G} {H} {K} →
      associative-comp-hom-species-𝔽 F G H K)
    ( λ {l1} {l2} {F} {G} → left-unit-law-comp-hom-species-𝔽 F G)
    ( λ {l1} {l2} {F} {G} → right-unit-law-comp-hom-species-𝔽 F G)