# Morphisms of species of types

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

Created on 2023-03-21.

module species.morphisms-species-of-types where

Imports
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.torsorial-type-families
open import foundation.universe-levels

open import species.species-of-types


### Idea

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

## Definitions

### Morphisms of species

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

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

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


### Homotopies between morphisms of species

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

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


## Properties

### Homotopies characterize the identity type of morphisms of species

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

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

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

eq-htpy-hom-species-types :
{l1 l2 l3 : Level} {F : species-types l1 l2} {G : species-types l1 l3}
{f g : hom-species-types F G} → htpy-hom-species-types f g → Id f g
eq-htpy-hom-species-types {f = f} {g = g} =
map-inv-is-equiv (is-equiv-htpy-eq-hom-species-types f g)


### Associativity of composition

module _
{l1 l2 l3 l4 l5 : Level}
{F : species-types l1 l2} {G : species-types l1 l3}
{H : species-types l1 l4} {K : species-types l1 l5}
(h : hom-species-types H K)
(g : hom-species-types G H)
(f : hom-species-types F G)
where

associative-comp-hom-species-types :
comp-hom-species-types (comp-hom-species-types h g) f ＝
comp-hom-species-types h (comp-hom-species-types g f)
associative-comp-hom-species-types = refl


### Unit laws of composition

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

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