The precategory of finite species

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

Created on 2023-03-21.
Last modified on 2024-03-11.

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)

Recent changes