# Morphisms of finite species

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

Created on 2023-03-21.

module species.morphisms-finite-species where

Imports
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import species.species-of-finite-types

open import univalent-combinatorics.finite-types


## Idea

A homomorphism between two finite species is a pointwise family of maps.

## Definitions

### The type of morphisms between finite species

hom-species-𝔽 :
{l1 l2 l3 : Level} → species-𝔽 l1 l2 → species-𝔽 l1 l3 →
UU (lsuc l1 ⊔ l2 ⊔ l3)
hom-species-𝔽 {l1} F G = (X : 𝔽 l1) → type-𝔽 (F X) → type-𝔽 (G X)


### The identity morphisms of finite species

id-hom-species-𝔽 :
{l1 l2 : Level} (F : species-𝔽 l1 l2) → hom-species-𝔽 F F
id-hom-species-𝔽 F = λ X x → x


### Composition of morphisms of finite species

comp-hom-species-𝔽 :
{l1 l2 l3 l4 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(H : species-𝔽 l1 l4) → hom-species-𝔽 G H →
hom-species-𝔽 F G → hom-species-𝔽 F H
comp-hom-species-𝔽 F G H f g X = (f X) ∘ (g X)


### Homotopies of morphisms of finite species

htpy-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3) →
(hom-species-𝔽 F G) → (hom-species-𝔽 F G) →
UU (lsuc l1 ⊔ l2 ⊔ l3)
htpy-hom-species-𝔽 {l1} F G f g = (X : 𝔽 l1) → (f X) ~ (g X)

refl-htpy-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3) →
(f : hom-species-𝔽 F G) → htpy-hom-species-𝔽 F G f f
refl-htpy-hom-species-𝔽 F G f X = refl-htpy


## Properties

### Associativity of composition of homomorphisms of finite species

module _
{l1 l2 l3 l4 l5 : Level}
(F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(H : species-𝔽 l1 l4) (K : species-𝔽 l1 l5)
where

associative-comp-hom-species-𝔽 :
(h : hom-species-𝔽 H K) (g : hom-species-𝔽 G H) (f : hom-species-𝔽 F G) →
comp-hom-species-𝔽 F G K (comp-hom-species-𝔽 G H K h g) f ＝
comp-hom-species-𝔽 F H K h (comp-hom-species-𝔽 F G H g f)
associative-comp-hom-species-𝔽 h g f = refl


### The unit laws for composition of homomorphisms of finite species

left-unit-law-comp-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(f : hom-species-𝔽 F G) →
Id (comp-hom-species-𝔽 F G G (id-hom-species-𝔽 G) f) f
left-unit-law-comp-hom-species-𝔽 F G f = refl

right-unit-law-comp-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(f : hom-species-𝔽 F G) →
Id (comp-hom-species-𝔽 F F G f (id-hom-species-𝔽 F)) f
right-unit-law-comp-hom-species-𝔽 F G f = refl


### Characterization of the identity type of homomorphisms of finite species

htpy-eq-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(f g : hom-species-𝔽 F G) →
Id f g → htpy-hom-species-𝔽 F G f g
htpy-eq-hom-species-𝔽 F G f g refl X y = refl

is-torsorial-htpy-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(f : hom-species-𝔽 F G) → is-torsorial (htpy-hom-species-𝔽 F G f)
is-torsorial-htpy-hom-species-𝔽 F G f =
is-torsorial-Eq-Π (λ X → is-torsorial-htpy (f X))

is-equiv-htpy-eq-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(f g : hom-species-𝔽 F G) →
is-equiv (htpy-eq-hom-species-𝔽 F G f g)
is-equiv-htpy-eq-hom-species-𝔽 F G f =
fundamental-theorem-id
( is-torsorial-htpy-hom-species-𝔽 F G f)
( λ g → htpy-eq-hom-species-𝔽 F G f g)

extensionality-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3)
(f g : hom-species-𝔽 F G) →
Id f g ≃ htpy-hom-species-𝔽 F G f g
pr1 (extensionality-hom-species-𝔽 F G f g) =
htpy-eq-hom-species-𝔽 F G f g
pr2 (extensionality-hom-species-𝔽 F G f g) =
is-equiv-htpy-eq-hom-species-𝔽 F G f g


### The type of homomorphisms of finite species is a set

is-set-hom-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3) →
is-set (hom-species-𝔽 F G)
is-set-hom-species-𝔽 F G f g =
is-prop-equiv
( extensionality-hom-species-𝔽 F G f g)
( is-prop-Π
( λ X →
is-prop-Π
( λ x p q →
is-set-is-finite (is-finite-type-𝔽 (G X)) (f X x) (g X x) p q)))

hom-set-species-𝔽 :
{l1 l2 l3 : Level} (F : species-𝔽 l1 l2) (G : species-𝔽 l1 l3) →
Set (lsuc l1 ⊔ l2 ⊔ l3)
pr1 (hom-set-species-𝔽 F G) = hom-species-𝔽 F G
pr2 (hom-set-species-𝔽 F G) = is-set-hom-species-𝔽 F G