The precategory of finite species

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

Created on 2023-03-21.
Last modified on 2023-09-26.

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

open import foundation.universe-levels

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


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


species-𝔽-Large-Precategory :
  (l1 : Level) 
  Large-Precategory  l  lsuc l1  lsuc l)  l2 l3  lsuc l1  l2  l3)
obj-Large-Precategory (species-𝔽-Large-Precategory l1) = species-𝔽 l1
hom-set-Large-Precategory (species-𝔽-Large-Precategory l1) = hom-set-species-𝔽
comp-hom-Large-Precategory (species-𝔽-Large-Precategory l1) {X = F} {G} {H} =
  comp-hom-species-𝔽 F G H
id-hom-Large-Precategory (species-𝔽-Large-Precategory l1) {X = F} =
  id-hom-species-𝔽 F
  ( species-𝔽-Large-Precategory l1) {X = F} {G} {H} {K} h g f =
  associative-comp-hom-species-𝔽 F G H K h g f
  ( species-𝔽-Large-Precategory l1) {X = F} {G} f =
  left-unit-law-comp-hom-species-𝔽 F G f
  ( species-𝔽-Large-Precategory l1) {X = F} {G} f =
  right-unit-law-comp-hom-species-𝔽 F G f

Recent changes