# Equivalences of types equipped with endomorphisms

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

Created on 2022-05-07.

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

Imports
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


## Definition

### The predicate of being an equivalence of types equipped with endomorphisms

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

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

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

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

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

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

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

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))