# Equivalences of types equipped with endomorphisms ```agda module structured-types.equivalences-types-equipped-with-endomorphisms where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-functions 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.function-types 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.subtype-identity-principle open import foundation.torsorial-type-families open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels open import structured-types.morphisms-types-equipped-with-endomorphisms open import structured-types.types-equipped-with-endomorphisms ``` </details> ## Definition ### The predicate of being an equivalence of types equipped with endomorphisms ```agda module _ {l1 l2 : Level} (X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2) where is-equiv-hom-Type-With-Endomorphism : hom-Type-With-Endomorphism X Y → UU (l1 ⊔ l2) is-equiv-hom-Type-With-Endomorphism h = is-equiv (map-hom-Type-With-Endomorphism X Y h) ``` ### Equivalences of types equipped with endomorphisms ```agda module _ {l1 l2 : Level} (X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2) where equiv-Type-With-Endomorphism : UU (l1 ⊔ l2) equiv-Type-With-Endomorphism = Σ ( type-Type-With-Endomorphism X ≃ type-Type-With-Endomorphism Y) ( λ e → coherence-square-maps ( map-equiv e) ( endomorphism-Type-With-Endomorphism X) ( endomorphism-Type-With-Endomorphism Y) ( map-equiv e)) equiv-Type-With-Endomorphism' : UU (l1 ⊔ l2) equiv-Type-With-Endomorphism' = Σ (hom-Type-With-Endomorphism X Y) (is-equiv-hom-Type-With-Endomorphism X Y) compute-equiv-Type-With-Endomorphism : equiv-Type-With-Endomorphism' ≃ equiv-Type-With-Endomorphism compute-equiv-Type-With-Endomorphism = equiv-right-swap-Σ equiv-equiv-Type-With-Endomorphism : equiv-Type-With-Endomorphism → type-Type-With-Endomorphism X ≃ type-Type-With-Endomorphism Y equiv-equiv-Type-With-Endomorphism e = pr1 e map-equiv-Type-With-Endomorphism : equiv-Type-With-Endomorphism → type-Type-With-Endomorphism X → type-Type-With-Endomorphism Y map-equiv-Type-With-Endomorphism e = map-equiv (equiv-equiv-Type-With-Endomorphism e) coherence-square-equiv-Type-With-Endomorphism : (e : equiv-Type-With-Endomorphism) → coherence-square-maps ( map-equiv-Type-With-Endomorphism e) ( endomorphism-Type-With-Endomorphism X) ( endomorphism-Type-With-Endomorphism Y) ( map-equiv-Type-With-Endomorphism e) coherence-square-equiv-Type-With-Endomorphism e = pr2 e hom-equiv-Type-With-Endomorphism : equiv-Type-With-Endomorphism → hom-Type-With-Endomorphism X Y pr1 (hom-equiv-Type-With-Endomorphism e) = map-equiv-Type-With-Endomorphism e pr2 (hom-equiv-Type-With-Endomorphism e) = coherence-square-equiv-Type-With-Endomorphism e is-equiv-equiv-Type-With-Endomorphism : (e : equiv-Type-With-Endomorphism) → is-equiv-hom-Type-With-Endomorphism X Y (hom-equiv-Type-With-Endomorphism e) is-equiv-equiv-Type-With-Endomorphism e = is-equiv-map-equiv (equiv-equiv-Type-With-Endomorphism e) ``` ### The identity equivalence ```agda module _ {l1 : Level} (X : Type-With-Endomorphism l1) where id-equiv-Type-With-Endomorphism : equiv-Type-With-Endomorphism X X pr1 id-equiv-Type-With-Endomorphism = id-equiv pr2 id-equiv-Type-With-Endomorphism = refl-htpy ``` ### Composition for equivalences of types equipped with endomorphisms ```agda comp-equiv-Type-With-Endomorphism : {l1 l2 l3 : Level} (X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2) (Z : Type-With-Endomorphism l3) → equiv-Type-With-Endomorphism Y Z → equiv-Type-With-Endomorphism X Y → equiv-Type-With-Endomorphism X Z pr1 (comp-equiv-Type-With-Endomorphism X Y Z f e) = pr1 f ∘e pr1 e pr2 (comp-equiv-Type-With-Endomorphism X Y Z f e) = pasting-horizontal-coherence-square-maps ( map-equiv-Type-With-Endomorphism X Y e) ( map-equiv-Type-With-Endomorphism Y Z f) ( endomorphism-Type-With-Endomorphism X) ( endomorphism-Type-With-Endomorphism Y) ( endomorphism-Type-With-Endomorphism Z) ( map-equiv-Type-With-Endomorphism X Y e) ( map-equiv-Type-With-Endomorphism Y Z f) ( coherence-square-equiv-Type-With-Endomorphism X Y e) ( coherence-square-equiv-Type-With-Endomorphism Y Z f) ``` ### Inverses of equivalences of types equipped with endomorphisms ```agda inv-equiv-Type-With-Endomorphism : {l1 l2 : Level} (X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2) → equiv-Type-With-Endomorphism X Y → equiv-Type-With-Endomorphism Y X pr1 (inv-equiv-Type-With-Endomorphism X Y e) = inv-equiv (equiv-equiv-Type-With-Endomorphism X Y e) pr2 (inv-equiv-Type-With-Endomorphism X Y e) = horizontal-inv-equiv-coherence-square-maps ( equiv-equiv-Type-With-Endomorphism X Y e) ( endomorphism-Type-With-Endomorphism X) ( endomorphism-Type-With-Endomorphism Y) ( equiv-equiv-Type-With-Endomorphism X Y e) ( coherence-square-equiv-Type-With-Endomorphism X Y e) ``` ### Homotopies of equivalences of types equipped with endomorphisms ```agda module _ {l1 l2 : Level} (X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2) where htpy-equiv-Type-With-Endomorphism : (e f : equiv-Type-With-Endomorphism X Y) → UU (l1 ⊔ l2) htpy-equiv-Type-With-Endomorphism e f = htpy-hom-Type-With-Endomorphism X Y ( hom-equiv-Type-With-Endomorphism X Y e) ( hom-equiv-Type-With-Endomorphism X Y f) refl-htpy-equiv-Type-With-Endomorphism : ( e : equiv-Type-With-Endomorphism X Y) → htpy-equiv-Type-With-Endomorphism e e refl-htpy-equiv-Type-With-Endomorphism e = refl-htpy-hom-Type-With-Endomorphism X Y ( hom-equiv-Type-With-Endomorphism X Y e) htpy-eq-equiv-Type-With-Endomorphism : (e f : equiv-Type-With-Endomorphism X Y) → e = f → htpy-equiv-Type-With-Endomorphism e f htpy-eq-equiv-Type-With-Endomorphism e .e refl = refl-htpy-equiv-Type-With-Endomorphism e is-torsorial-htpy-equiv-Type-With-Endomorphism : (e : equiv-Type-With-Endomorphism X Y) → is-torsorial (htpy-equiv-Type-With-Endomorphism e) is-torsorial-htpy-equiv-Type-With-Endomorphism e = is-contr-equiv ( Σ ( Σ ( hom-Type-With-Endomorphism X Y) ( λ f → is-equiv (map-hom-Type-With-Endomorphism X Y f))) ( λ f → htpy-hom-Type-With-Endomorphism X Y ( hom-equiv-Type-With-Endomorphism X Y e) ( pr1 f))) ( equiv-Σ ( λ f → htpy-hom-Type-With-Endomorphism X Y ( hom-equiv-Type-With-Endomorphism X Y e) ( pr1 f)) ( equiv-right-swap-Σ) ( λ f → id-equiv)) ( is-torsorial-Eq-subtype ( is-torsorial-htpy-hom-Type-With-Endomorphism X Y ( hom-equiv-Type-With-Endomorphism X Y e)) ( λ f → is-property-is-equiv (pr1 f)) ( hom-equiv-Type-With-Endomorphism X Y e) ( refl-htpy-hom-Type-With-Endomorphism X Y ( hom-equiv-Type-With-Endomorphism X Y e)) ( pr2 (pr1 e))) is-equiv-htpy-eq-equiv-Type-With-Endomorphism : (e f : equiv-Type-With-Endomorphism X Y) → is-equiv (htpy-eq-equiv-Type-With-Endomorphism e f) is-equiv-htpy-eq-equiv-Type-With-Endomorphism e = fundamental-theorem-id ( is-torsorial-htpy-equiv-Type-With-Endomorphism e) ( htpy-eq-equiv-Type-With-Endomorphism e) extensionality-equiv-Type-With-Endomorphism : (e f : equiv-Type-With-Endomorphism X Y) → (e = f) ≃ htpy-equiv-Type-With-Endomorphism e f pr1 (extensionality-equiv-Type-With-Endomorphism e f) = htpy-eq-equiv-Type-With-Endomorphism e f pr2 (extensionality-equiv-Type-With-Endomorphism e f) = is-equiv-htpy-eq-equiv-Type-With-Endomorphism e f eq-htpy-equiv-Type-With-Endomorphism : (e f : equiv-Type-With-Endomorphism X Y) → htpy-equiv-Type-With-Endomorphism e f → e = f eq-htpy-equiv-Type-With-Endomorphism e f = map-inv-equiv (extensionality-equiv-Type-With-Endomorphism e f) ``` ## Properties ### Unit laws for composition of equivalences of types equipped with endomorphisms ```agda module _ {l1 l2 : Level} (X : Type-With-Endomorphism l1) (Y : Type-With-Endomorphism l2) where left-unit-law-comp-equiv-Type-With-Endomorphism : (e : equiv-Type-With-Endomorphism X Y) → comp-equiv-Type-With-Endomorphism X Y Y ( id-equiv-Type-With-Endomorphism Y) e = e left-unit-law-comp-equiv-Type-With-Endomorphism e = eq-htpy-equiv-Type-With-Endomorphism X Y ( comp-equiv-Type-With-Endomorphism X Y Y ( id-equiv-Type-With-Endomorphism Y) ( e)) ( e) ( pair ( refl-htpy) ( λ x → inv ( ( right-unit) ∙ ( right-unit) ∙ ( ap-id ( coherence-square-equiv-Type-With-Endomorphism X Y e x))))) right-unit-law-comp-equiv-Type-With-Endomorphism : (e : equiv-Type-With-Endomorphism X Y) → comp-equiv-Type-With-Endomorphism X X Y e ( id-equiv-Type-With-Endomorphism X) = e right-unit-law-comp-equiv-Type-With-Endomorphism e = eq-htpy-equiv-Type-With-Endomorphism X Y ( comp-equiv-Type-With-Endomorphism X X Y e ( id-equiv-Type-With-Endomorphism X)) ( e) ( pair ( refl-htpy) ( λ x → inv right-unit)) ``` ### Extensionality of types equipped with endomorphisms ```agda module _ {l1 : Level} (X : Type-With-Endomorphism l1) where equiv-eq-Type-With-Endomorphism : ( Y : Type-With-Endomorphism l1) → X = Y → equiv-Type-With-Endomorphism X Y equiv-eq-Type-With-Endomorphism .X refl = id-equiv-Type-With-Endomorphism X is-torsorial-equiv-Type-With-Endomorphism : is-torsorial (equiv-Type-With-Endomorphism X) is-torsorial-equiv-Type-With-Endomorphism = is-torsorial-Eq-structure ( is-torsorial-equiv (type-Type-With-Endomorphism X)) ( type-Type-With-Endomorphism X , id-equiv) ( is-torsorial-htpy (endomorphism-Type-With-Endomorphism X)) is-equiv-equiv-eq-Type-With-Endomorphism : ( Y : Type-With-Endomorphism l1) → is-equiv (equiv-eq-Type-With-Endomorphism Y) is-equiv-equiv-eq-Type-With-Endomorphism = fundamental-theorem-id is-torsorial-equiv-Type-With-Endomorphism equiv-eq-Type-With-Endomorphism extensionality-Type-With-Endomorphism : (Y : Type-With-Endomorphism l1) → (X = Y) ≃ equiv-Type-With-Endomorphism X Y pr1 (extensionality-Type-With-Endomorphism Y) = equiv-eq-Type-With-Endomorphism Y pr2 (extensionality-Type-With-Endomorphism Y) = is-equiv-equiv-eq-Type-With-Endomorphism Y eq-equiv-Type-With-Endomorphism : (Y : Type-With-Endomorphism l1) → equiv-Type-With-Endomorphism X Y → X = Y eq-equiv-Type-With-Endomorphism Y = map-inv-is-equiv (is-equiv-equiv-eq-Type-With-Endomorphism Y) module _ {l : Level} (X : Type-With-Endomorphism l) (Y : Type-With-Endomorphism l) (Z : Type-With-Endomorphism l) where preserves-concat-equiv-eq-Type-With-Endomorphism : (p : X = Y) (q : Y = Z) → ( equiv-eq-Type-With-Endomorphism X Z (p ∙ q)) = ( comp-equiv-Type-With-Endomorphism X Y Z ( equiv-eq-Type-With-Endomorphism Y Z q) ( equiv-eq-Type-With-Endomorphism X Y p)) preserves-concat-equiv-eq-Type-With-Endomorphism refl q = inv ( right-unit-law-comp-equiv-Type-With-Endomorphism X Z ( equiv-eq-Type-With-Endomorphism X Z q)) ```