# Morphisms of types equipped with endomorphisms

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-07.

module structured-types.morphisms-types-equipped-with-endomorphisms where

Imports
open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-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.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import structured-types.types-equipped-with-endomorphisms


## Idea

Consider two types equipped with an endomorphism (X,f) and (Y,g). A morphism from (X,f) to (Y,g) consists of a map h : X → Y equipped with a homotopy witnessing that the square

      h
X -----> Y
|        |
f|        |g
V        V
X -----> Y
h


## Definition

### Morphisms of types equipped with endomorphisms

module _
{l1 l2 : Level}
(X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2)
where

hom-Type-With-Endomorphism : UU (l1 ⊔ l2)
hom-Type-With-Endomorphism =
Σ ( type-Type-With-Endomorphism X → type-Type-With-Endomorphism Y)
( λ f →
coherence-square-maps
( f)
( endomorphism-Type-With-Endomorphism X)
( endomorphism-Type-With-Endomorphism Y)
( f))

map-hom-Type-With-Endomorphism :
hom-Type-With-Endomorphism →
type-Type-With-Endomorphism X → type-Type-With-Endomorphism Y
map-hom-Type-With-Endomorphism = pr1

coherence-square-hom-Type-With-Endomorphism :
(f : hom-Type-With-Endomorphism) →
coherence-square-maps
( map-hom-Type-With-Endomorphism f)
( endomorphism-Type-With-Endomorphism X)
( endomorphism-Type-With-Endomorphism Y)
( map-hom-Type-With-Endomorphism f)
coherence-square-hom-Type-With-Endomorphism = pr2


### Homotopies of morphisms of types equipped with endomorphisms

module _
{l1 l2 : Level}
(X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2)
where

htpy-hom-Type-With-Endomorphism :
(f g : hom-Type-With-Endomorphism X Y) → UU (l1 ⊔ l2)
htpy-hom-Type-With-Endomorphism f g =
Σ ( map-hom-Type-With-Endomorphism X Y f ~
map-hom-Type-With-Endomorphism X Y g)
( λ H →
( ( H ·r endomorphism-Type-With-Endomorphism X) ∙h
( coherence-square-hom-Type-With-Endomorphism X Y g)) ~
( ( coherence-square-hom-Type-With-Endomorphism X Y f) ∙h
( endomorphism-Type-With-Endomorphism Y ·l H)))

refl-htpy-hom-Type-With-Endomorphism :
(f : hom-Type-With-Endomorphism X Y) → htpy-hom-Type-With-Endomorphism f f
pr1 (refl-htpy-hom-Type-With-Endomorphism f) = refl-htpy
pr2 (refl-htpy-hom-Type-With-Endomorphism f) = inv-htpy-right-unit-htpy

htpy-eq-hom-Type-With-Endomorphism :
(f g : hom-Type-With-Endomorphism X Y) →
f ＝ g → htpy-hom-Type-With-Endomorphism f g
htpy-eq-hom-Type-With-Endomorphism f .f refl =
refl-htpy-hom-Type-With-Endomorphism f

is-torsorial-htpy-hom-Type-With-Endomorphism :
(f : hom-Type-With-Endomorphism X Y) →
is-torsorial (htpy-hom-Type-With-Endomorphism f)
is-torsorial-htpy-hom-Type-With-Endomorphism f =
is-torsorial-Eq-structure
( is-torsorial-htpy (map-hom-Type-With-Endomorphism X Y f))
( map-hom-Type-With-Endomorphism X Y f , refl-htpy)
( is-contr-equiv
( Σ ( coherence-square-maps
( map-hom-Type-With-Endomorphism X Y f)
( endomorphism-Type-With-Endomorphism X)
( endomorphism-Type-With-Endomorphism Y)
( map-hom-Type-With-Endomorphism X Y f))
( λ H → H ~ coherence-square-hom-Type-With-Endomorphism X Y f))
( equiv-tot (λ H → equiv-concat-htpy' H right-unit-htpy))
( is-torsorial-htpy'
( coherence-square-hom-Type-With-Endomorphism X Y f)))

is-equiv-htpy-eq-hom-Type-With-Endomorphism :
(f g : hom-Type-With-Endomorphism X Y) →
is-equiv (htpy-eq-hom-Type-With-Endomorphism f g)
is-equiv-htpy-eq-hom-Type-With-Endomorphism f =
fundamental-theorem-id
( is-torsorial-htpy-hom-Type-With-Endomorphism f)
( htpy-eq-hom-Type-With-Endomorphism f)

extensionality-hom-Type-With-Endomorphism :
(f g : hom-Type-With-Endomorphism X Y) →
(f ＝ g) ≃ htpy-hom-Type-With-Endomorphism f g
pr1 (extensionality-hom-Type-With-Endomorphism f g) =
htpy-eq-hom-Type-With-Endomorphism f g
pr2 (extensionality-hom-Type-With-Endomorphism f g) =
is-equiv-htpy-eq-hom-Type-With-Endomorphism f g

eq-htpy-hom-Type-With-Endomorphism :
( f g : hom-Type-With-Endomorphism X Y) →
htpy-hom-Type-With-Endomorphism f g → f ＝ g
eq-htpy-hom-Type-With-Endomorphism f g =
map-inv-equiv (extensionality-hom-Type-With-Endomorphism f g)