# Morphisms of types equipped with automorphisms ```agda module structured-types.morphisms-types-equipped-with-automorphisms where ``` <details><summary>Imports</summary> ```agda open import foundation.commuting-squares-of-maps open import foundation.equivalences open import foundation.identity-types open import foundation.torsorial-type-families open import foundation.universe-levels open import structured-types.morphisms-types-equipped-with-endomorphisms open import structured-types.types-equipped-with-automorphisms ``` </details> ## Idea Consider two [types equipped with an automorphism](structured-types.types-equipped-with-automorphisms.md) `(X,e)` and `(Y,f)`. A **morphism** from `(X,e)` to `(Y,f)` consists of a map `h : X → Y` equipped with a [homotopy](foundation-core.homotopies.md) witnessing that the square ```text h X -----> Y | | e| |f ∨ ∨ X -----> Y h ``` [commutes](foundation.commuting-squares-of-maps.md). ## Definition ### Morphisms of types equipped with automorphisms ```agda module _ {l1 l2 : Level} (X : Type-With-Automorphism l1) (Y : Type-With-Automorphism l2) where hom-Type-With-Automorphism : UU (l1 ⊔ l2) hom-Type-With-Automorphism = hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) map-hom-Type-With-Automorphism : hom-Type-With-Automorphism → type-Type-With-Automorphism X → type-Type-With-Automorphism Y map-hom-Type-With-Automorphism = map-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) coherence-square-hom-Type-With-Automorphism : (f : hom-Type-With-Automorphism) → coherence-square-maps ( map-hom-Type-With-Automorphism f) ( map-Type-With-Automorphism X) ( map-Type-With-Automorphism Y) ( map-hom-Type-With-Automorphism f) coherence-square-hom-Type-With-Automorphism = coherence-square-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) ``` ### Homotopies of morphisms of types equipped with automorphisms ```agda module _ {l1 l2 : Level} (X : Type-With-Automorphism l1) (Y : Type-With-Automorphism l2) where htpy-hom-Type-With-Automorphism : (f g : hom-Type-With-Automorphism X Y) → UU (l1 ⊔ l2) htpy-hom-Type-With-Automorphism = htpy-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) refl-htpy-hom-Type-With-Automorphism : (f : hom-Type-With-Automorphism X Y) → htpy-hom-Type-With-Automorphism f f refl-htpy-hom-Type-With-Automorphism = refl-htpy-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) htpy-eq-hom-Type-With-Automorphism : (f g : hom-Type-With-Automorphism X Y) → f = g → htpy-hom-Type-With-Automorphism f g htpy-eq-hom-Type-With-Automorphism = htpy-eq-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) is-torsorial-htpy-hom-Type-With-Automorphism : (f : hom-Type-With-Automorphism X Y) → is-torsorial (htpy-hom-Type-With-Automorphism f) is-torsorial-htpy-hom-Type-With-Automorphism = is-torsorial-htpy-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) is-equiv-htpy-eq-hom-Type-With-Automorphism : (f g : hom-Type-With-Automorphism X Y) → is-equiv (htpy-eq-hom-Type-With-Automorphism f g) is-equiv-htpy-eq-hom-Type-With-Automorphism = is-equiv-htpy-eq-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) extensionality-hom-Type-With-Automorphism : (f g : hom-Type-With-Automorphism X Y) → (f = g) ≃ htpy-hom-Type-With-Automorphism f g extensionality-hom-Type-With-Automorphism = extensionality-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) eq-htpy-hom-Type-With-Automorphism : ( f g : hom-Type-With-Automorphism X Y) → htpy-hom-Type-With-Automorphism f g → f = g eq-htpy-hom-Type-With-Automorphism = eq-htpy-hom-Type-With-Endomorphism ( type-with-endomorphism-Type-With-Automorphism X) ( type-with-endomorphism-Type-With-Automorphism Y) ```