Morphisms of species of types

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

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

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

  inv-associative-comp-hom-species-types :
    comp-hom-species-types h (comp-hom-species-types g f) 
    comp-hom-species-types (comp-hom-species-types h g) f
  inv-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

Recent changes