# Equivalences

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, maybemabeline, Julian KG, Raymond Baker, fernabnor and louismntnu.

Created on 2022-02-04.

module foundation-core.equivalences where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.cartesian-product-types
open import foundation-core.coherently-invertible-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.invertible-maps
open import foundation-core.retractions
open import foundation-core.sections


## Idea

An equivalence is a map that has a section and a (separate) retraction. This condition is also called being biinvertible.

The condition of biinvertibility may look odd: Why not say that an equivalence is a map that has a 2-sided inverse? The reason is that the condition of invertibility is structure, whereas the condition of being biinvertible is a property. To quickly see this: if f is an equivalence, then it has up to homotopy only one section, and it has up to homotopy only one retraction.

## Definition

### The predicate of being an equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-equiv : (A → B) → UU (l1 ⊔ l2)
is-equiv f = section f × retraction f


### Components of a proof of equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-equiv f)
where

section-is-equiv : section f
section-is-equiv = pr1 H

retraction-is-equiv : retraction f
retraction-is-equiv = pr2 H

map-section-is-equiv : B → A
map-section-is-equiv = map-section f section-is-equiv

map-retraction-is-equiv : B → A
map-retraction-is-equiv = map-retraction f retraction-is-equiv

is-section-map-section-is-equiv : is-section f map-section-is-equiv
is-section-map-section-is-equiv = is-section-map-section f section-is-equiv

is-retraction-map-retraction-is-equiv :
is-retraction f map-retraction-is-equiv
is-retraction-map-retraction-is-equiv =
is-retraction-map-retraction f retraction-is-equiv


### Equivalences

module _
{l1 l2 : Level} (A : UU l1) (B : UU l2)
where

equiv : UU (l1 ⊔ l2)
equiv = Σ (A → B) is-equiv

infix 6 _≃_

_≃_ : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
A ≃ B = equiv A B


### Components of an equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
where

map-equiv : A → B
map-equiv = pr1 e

is-equiv-map-equiv : is-equiv map-equiv
is-equiv-map-equiv = pr2 e

section-map-equiv : section map-equiv
section-map-equiv = section-is-equiv is-equiv-map-equiv

map-section-map-equiv : B → A
map-section-map-equiv = map-section map-equiv section-map-equiv

is-section-map-section-map-equiv :
is-section map-equiv map-section-map-equiv
is-section-map-section-map-equiv =
is-section-map-section map-equiv section-map-equiv

retraction-map-equiv : retraction map-equiv
retraction-map-equiv = retraction-is-equiv is-equiv-map-equiv

map-retraction-map-equiv : B → A
map-retraction-map-equiv = map-retraction map-equiv retraction-map-equiv

is-retraction-map-retraction-map-equiv :
is-retraction map-equiv map-retraction-map-equiv
is-retraction-map-retraction-map-equiv =
is-retraction-map-retraction map-equiv retraction-map-equiv


### The identity equivalence

module _
{l : Level} {A : UU l}
where

is-equiv-id : is-equiv (id {l} {A})
pr1 (pr1 is-equiv-id) = id
pr2 (pr1 is-equiv-id) = refl-htpy
pr1 (pr2 is-equiv-id) = id
pr2 (pr2 is-equiv-id) = refl-htpy

id-equiv : A ≃ A
pr1 id-equiv = id
pr2 id-equiv = is-equiv-id


## Properties

### A map is invertible if and only if it is an equivalence

Proof: It is clear that if a map is invertible, then it is also biinvertible, and hence an equivalence.

For the converse, suppose that f : A → B is an equivalence with section g : B → A equipped with G : f ∘ g ~ id, and retraction h : B → A equipped with H : h ∘ f ~ id. We claim that the map g : B → A is also a retraction. To see this, we concatenate the following homotopies

         H⁻¹ ·r g ·r f                  h ·l G ·r f           H
g ∘ h ---------------> h ∘ f ∘ g ∘ f -------------> h ∘ f -----> id.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

is-equiv-is-invertible' : is-invertible f → is-equiv f
is-equiv-is-invertible' (g , H , K) = ((g , H) , (g , K))

is-equiv-is-invertible :
(g : B → A) (H : f ∘ g ~ id) (K : g ∘ f ~ id) → is-equiv f
is-equiv-is-invertible g H K = is-equiv-is-invertible' (g , H , K)

is-retraction-map-section-is-equiv :
(H : is-equiv f) → is-retraction f (map-section-is-equiv H)
is-retraction-map-section-is-equiv H =
( ( inv-htpy
( ( is-retraction-map-retraction-is-equiv H) ·r
( map-section-is-equiv H ∘ f))) ∙h
( map-retraction-is-equiv H ·l is-section-map-section-is-equiv H ·r f)) ∙h
( is-retraction-map-retraction-is-equiv H)

is-invertible-is-equiv : is-equiv f → is-invertible f
pr1 (is-invertible-is-equiv H) = map-section-is-equiv H
pr1 (pr2 (is-invertible-is-equiv H)) = is-section-map-section-is-equiv H
pr2 (pr2 (is-invertible-is-equiv H)) = is-retraction-map-section-is-equiv H


### Coherently invertible maps are equivalences

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

is-equiv-is-coherently-invertible :
is-coherently-invertible f → is-equiv f
is-equiv-is-coherently-invertible H =
is-equiv-is-invertible' (is-invertible-is-coherently-invertible H)

is-equiv-is-transpose-coherently-invertible :
is-transpose-coherently-invertible f → is-equiv f
is-equiv-is-transpose-coherently-invertible H =
is-equiv-is-invertible'
( is-invertible-is-transpose-coherently-invertible H)


The following maps are not simple constructions and should not be computed with. Therefore, we mark them as abstract.

  abstract
is-coherently-invertible-is-equiv :
is-equiv f → is-coherently-invertible f
is-coherently-invertible-is-equiv =
is-coherently-invertible-is-invertible ∘ is-invertible-is-equiv

abstract
is-transpose-coherently-invertible-is-equiv :
is-equiv f → is-transpose-coherently-invertible f
is-transpose-coherently-invertible-is-equiv =
is-transpose-coherently-invertible-is-invertible ∘ is-invertible-is-equiv


### Structure obtained from being coherently invertible

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-equiv f)
where

map-inv-is-equiv : B → A
map-inv-is-equiv = pr1 (is-invertible-is-equiv H)

is-section-map-inv-is-equiv : is-section f map-inv-is-equiv
is-section-map-inv-is-equiv =
is-section-map-inv-is-coherently-invertible-is-invertible
( is-invertible-is-equiv H)

is-retraction-map-inv-is-equiv : is-retraction f map-inv-is-equiv
is-retraction-map-inv-is-equiv =
is-retraction-map-inv-is-coherently-invertible-is-invertible
( is-invertible-is-equiv H)

coherence-map-inv-is-equiv :
coherence-is-coherently-invertible f
( map-inv-is-equiv)
( is-section-map-inv-is-equiv)
( is-retraction-map-inv-is-equiv)
coherence-map-inv-is-equiv =
coh-is-coherently-invertible-is-invertible (is-invertible-is-equiv H)

is-equiv-map-inv-is-equiv : is-equiv map-inv-is-equiv
is-equiv-map-inv-is-equiv =
is-equiv-is-invertible f
( is-retraction-map-inv-is-equiv)
( is-section-map-inv-is-equiv)


### The inverse of an equivalence is an equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
where

map-inv-equiv : B → A
map-inv-equiv = map-inv-is-equiv (is-equiv-map-equiv e)

is-section-map-inv-equiv : is-section (map-equiv e) map-inv-equiv
is-section-map-inv-equiv = is-section-map-inv-is-equiv (is-equiv-map-equiv e)

is-retraction-map-inv-equiv : is-retraction (map-equiv e) map-inv-equiv
is-retraction-map-inv-equiv =
is-retraction-map-inv-is-equiv (is-equiv-map-equiv e)

coherence-map-inv-equiv :
coherence-is-coherently-invertible
( map-equiv e)
( map-inv-equiv)
( is-section-map-inv-equiv)
( is-retraction-map-inv-equiv)
coherence-map-inv-equiv =
coherence-map-inv-is-equiv (is-equiv-map-equiv e)

is-equiv-map-inv-equiv : is-equiv map-inv-equiv
is-equiv-map-inv-equiv = is-equiv-map-inv-is-equiv (is-equiv-map-equiv e)

inv-equiv : B ≃ A
pr1 inv-equiv = map-inv-equiv
pr2 inv-equiv = is-equiv-map-inv-equiv


### The 3-for-2 property of equivalences

The 3-for-2 property of equivalences asserts that for any commuting triangle of maps

       h
A ------> B
\       /
f\     /g
\   /
∨ ∨
X,


if two of the three maps are equivalences, then so is the third.

We also record special cases of the 3-for-2 property of equivalences, where we only assume maps g : B → X and h : A → B. In this special case, we set f := g ∘ h and the triangle commutes by refl-htpy.

André Joyal proposed calling this property the 3-for-2 property, despite most mathematicians calling it the 2-out-of-3 property. The story goes that on the produce market is is common to advertise a discount as "3-for-2". If you buy two apples, then you get the third for free. Similarly, if you prove that two maps in a commuting triangle are equivalences, then you get the third for free.

#### The left map in a commuting triangle is an equivalence if the other two maps are equivalences

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (T : f ~ g ∘ h)
where

abstract
is-equiv-left-map-triangle : is-equiv h → is-equiv g → is-equiv f
pr1 (is-equiv-left-map-triangle H G) =
section-left-map-triangle f g h T
( section-is-equiv H)
( section-is-equiv G)
pr2 (is-equiv-left-map-triangle H G) =
retraction-left-map-triangle f g h T
( retraction-is-equiv G)
( retraction-is-equiv H)


#### The right map in a commuting triangle is an equivalence if the other two maps are equivalences

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
where

abstract
is-equiv-right-map-triangle :
is-equiv f → is-equiv h → is-equiv g
is-equiv-right-map-triangle
( section-f , retraction-f)
( (sh , is-section-sh) , retraction-h) =
( pair
( section-right-map-triangle f g h H section-f)
( retraction-left-map-triangle g f sh
( inv-htpy
( ( H ·r map-section h (sh , is-section-sh)) ∙h
( g ·l is-section-map-section h (sh , is-section-sh))))
( retraction-f)
( h , is-section-sh)))


#### If the left and right maps in a commuting triangle are equivalences, then the top map is an equivalence

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
where

section-is-equiv-top-map-triangle :
is-equiv g → is-equiv f → section h
section-is-equiv-top-map-triangle G F =
section-left-map-triangle h
( map-retraction-is-equiv G)
( f)
( inv-htpy
( ( map-retraction g (retraction-is-equiv G) ·l H) ∙h
( is-retraction-map-retraction g (retraction-is-equiv G) ·r h)))
( section-is-equiv F)
( g , is-retraction-map-retraction-is-equiv G)

map-section-is-equiv-top-map-triangle :
is-equiv g → is-equiv f → B → A
map-section-is-equiv-top-map-triangle G F =
map-section h (section-is-equiv-top-map-triangle G F)

abstract
is-equiv-top-map-triangle :
is-equiv g → is-equiv f → is-equiv h
is-equiv-top-map-triangle
( section-g , (rg , is-retraction-rg))
( section-f , retraction-f) =
( pair
( section-left-map-triangle h rg f
( inv-htpy
( ( map-retraction g (rg , is-retraction-rg) ·l H) ∙h
( is-retraction-map-retraction g (rg , is-retraction-rg) ·r h)))
( section-f)
( g , is-retraction-rg))
( retraction-top-map-triangle f g h H retraction-f))


#### Composites of equivalences are equivalences

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
where

abstract
is-equiv-comp :
(g : B → X) (h : A → B) → is-equiv h → is-equiv g → is-equiv (g ∘ h)
pr1 (is-equiv-comp g h (sh , rh) (sg , rg)) = section-comp g h sh sg
pr2 (is-equiv-comp g h (sh , rh) (sg , rg)) = retraction-comp g h rg rh

comp-equiv : B ≃ X → A ≃ B → A ≃ X
pr1 (comp-equiv g h) = map-equiv g ∘ map-equiv h
pr2 (comp-equiv g h) = is-equiv-comp (pr1 g) (pr1 h) (pr2 h) (pr2 g)

infixr 15 _∘e_
_∘e_ : B ≃ X → A ≃ B → A ≃ X
_∘e_ = comp-equiv


#### If a composite and its right factor are equivalences, then so is its left factor

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
where

is-equiv-left-factor :
(g : B → X) (h : A → B) →
is-equiv (g ∘ h) → is-equiv h → is-equiv g
is-equiv-left-factor g h is-equiv-gh is-equiv-h =
is-equiv-right-map-triangle (g ∘ h) g h refl-htpy is-equiv-gh is-equiv-h


#### If a composite and its left factor are equivalences, then so is its right factor

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
where

is-equiv-right-factor :
(g : B → X) (h : A → B) →
is-equiv g → is-equiv (g ∘ h) → is-equiv h
is-equiv-right-factor g h is-equiv-g is-equiv-gh =
is-equiv-top-map-triangle (g ∘ h) g h refl-htpy is-equiv-g is-equiv-gh


### Equivalences are closed under homotopies

We show that if f ~ g, then f is an equivalence if and only if g is an equivalence. Furthermore, we show that if f and g are homotopic equivaleces, then their inverses are also homotopic.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

abstract
is-equiv-htpy :
{f : A → B} (g : A → B) → f ~ g → is-equiv g → is-equiv f
pr1 (pr1 (is-equiv-htpy g G ((h , H) , (k , K)))) = h
pr2 (pr1 (is-equiv-htpy g G ((h , H) , (k , K)))) = (G ·r h) ∙h H
pr1 (pr2 (is-equiv-htpy g G ((h , H) , (k , K)))) = k
pr2 (pr2 (is-equiv-htpy g G ((h , H) , (k , K)))) = (k ·l G) ∙h K

is-equiv-htpy-equiv : {f : A → B} (e : A ≃ B) → f ~ map-equiv e → is-equiv f
is-equiv-htpy-equiv e H = is-equiv-htpy (map-equiv e) H (is-equiv-map-equiv e)

abstract
is-equiv-htpy' : (f : A → B) {g : A → B} → f ~ g → is-equiv f → is-equiv g
is-equiv-htpy' f H = is-equiv-htpy f (inv-htpy H)

is-equiv-htpy-equiv' : (e : A ≃ B) {g : A → B} → map-equiv e ~ g → is-equiv g
is-equiv-htpy-equiv' e H =
is-equiv-htpy' (map-equiv e) H (is-equiv-map-equiv e)

htpy-map-inv-is-equiv :
{f g : A → B} (H : f ~ g) (F : is-equiv f) (G : is-equiv g) →
map-inv-is-equiv F ~ map-inv-is-equiv G
htpy-map-inv-is-equiv H F G =
htpy-map-inv-is-invertible H
( is-invertible-is-equiv F)
( is-invertible-is-equiv G)


### Any retraction of an equivalence is an equivalence

abstract
is-equiv-is-retraction :
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} →
is-equiv f → (g ∘ f) ~ id → is-equiv g
is-equiv-is-retraction {A = A} {f = f} {g = g} is-equiv-f H =
is-equiv-right-map-triangle id g f (inv-htpy H) is-equiv-id is-equiv-f


### Any section of an equivalence is an equivalence

abstract
is-equiv-is-section :
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} →
is-equiv f → f ∘ g ~ id → is-equiv g
is-equiv-is-section {B = B} {f = f} {g = g} is-equiv-f H =
is-equiv-top-map-triangle id f g (inv-htpy H) is-equiv-f is-equiv-id


### If a section of f is an equivalence, then f is an equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

abstract
is-equiv-is-equiv-section :
(s : section f) → is-equiv (map-section f s) → is-equiv f
is-equiv-is-equiv-section (g , G) S = is-equiv-is-retraction S G


### If a retraction of f is an equivalence, then f is an equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

abstract
is-equiv-is-equiv-retraction :
(r : retraction f) → is-equiv (map-retraction f r) → is-equiv f
is-equiv-is-equiv-retraction (g , G) R = is-equiv-is-section R G


### Any section of an equivalence is homotopic to its inverse

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
where

htpy-map-inv-equiv-section :
(f : section (map-equiv e)) → map-inv-equiv e ~ map-section (map-equiv e) f
htpy-map-inv-equiv-section (f , H) =
(map-inv-equiv e ·l inv-htpy H) ∙h (is-retraction-map-inv-equiv e ·r f)


### Any retraction of an equivalence is homotopic to its inverse

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
where

htpy-map-inv-equiv-retraction :
(f : retraction (map-equiv e)) →
map-inv-equiv e ~ map-retraction (map-equiv e) f
htpy-map-inv-equiv-retraction (f , H) =
(inv-htpy H ·r map-inv-equiv e) ∙h (f ·l is-section-map-inv-equiv e)


### Equivalences in commuting squares

is-equiv-equiv :
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
{f : A → B} {g : X → Y} (i : A ≃ X) (j : B ≃ Y)
(H : (map-equiv j ∘ f) ~ (g ∘ map-equiv i)) → is-equiv g → is-equiv f
is-equiv-equiv {f = f} {g} i j H K =
is-equiv-right-factor
( map-equiv j)
( f)
( is-equiv-map-equiv j)
( is-equiv-left-map-triangle
( map-equiv j ∘ f)
( g)
( map-equiv i)
( H)
( is-equiv-map-equiv i)
( K))

is-equiv-equiv' :
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
{f : A → B} {g : X → Y} (i : A ≃ X) (j : B ≃ Y)
(H : (map-equiv j ∘ f) ~ (g ∘ map-equiv i)) → is-equiv f → is-equiv g
is-equiv-equiv' {f = f} {g} i j H K =
is-equiv-left-factor
( g)
( map-equiv i)
( is-equiv-left-map-triangle
( g ∘ map-equiv i)
( map-equiv j)
( f)
( inv-htpy H)
( K)
( is-equiv-map-equiv j))
( is-equiv-map-equiv i)


We will assume a commuting square

        h
A -----> C
|        |
f |        | g
∨        ∨
B -----> D
i

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
(f : A → B) (g : C → D) (h : A → C) (i : B → D) (H : (i ∘ f) ~ (g ∘ h))
where

abstract
is-equiv-top-is-equiv-left-square :
is-equiv i → is-equiv f → is-equiv g → is-equiv h
is-equiv-top-is-equiv-left-square Ei Ef Eg =
is-equiv-top-map-triangle (i ∘ f) g h H Eg (is-equiv-comp i f Ef Ei)

abstract
is-equiv-top-is-equiv-bottom-square :
is-equiv f → is-equiv g → is-equiv i → is-equiv h
is-equiv-top-is-equiv-bottom-square Ef Eg Ei =
is-equiv-top-map-triangle (i ∘ f) g h H Eg (is-equiv-comp i f Ef Ei)

abstract
is-equiv-bottom-is-equiv-top-square :
is-equiv f → is-equiv g → is-equiv h → is-equiv i
is-equiv-bottom-is-equiv-top-square Ef Eg Eh =
is-equiv-left-factor i f
( is-equiv-left-map-triangle (i ∘ f) g h H Eh Eg)
( Ef)

abstract
is-equiv-left-is-equiv-right-square :
is-equiv h → is-equiv i → is-equiv g → is-equiv f
is-equiv-left-is-equiv-right-square Eh Ei Eg =
is-equiv-right-factor i f Ei
( is-equiv-left-map-triangle (i ∘ f) g h H Eh Eg)

abstract
is-equiv-right-is-equiv-left-square :
is-equiv h → is-equiv i → is-equiv f → is-equiv g
is-equiv-right-is-equiv-left-square Eh Ei Ef =
is-equiv-right-map-triangle (i ∘ f) g h H (is-equiv-comp i f Ef Ei) Eh


### Equivalences are embeddings

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

abstract
is-emb-is-equiv :
{f : A → B} → is-equiv f → (x y : A) → is-equiv (ap f {x} {y})
is-emb-is-equiv H x y =
is-equiv-is-invertible'
( is-invertible-ap-is-coherently-invertible
( is-coherently-invertible-is-equiv H))

equiv-ap :
(e : A ≃ B) (x y : A) → (x ＝ y) ≃ (map-equiv e x ＝ map-equiv e y)
pr1 (equiv-ap e x y) = ap (map-equiv e)
pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y

map-inv-equiv-ap :
(e : A ≃ B) (x y : A) → map-equiv e x ＝ map-equiv e y → x ＝ y
map-inv-equiv-ap e x y = map-inv-equiv (equiv-ap e x y)


## Equivalence reasoning

Equivalences can be constructed by equational reasoning in the following way:

equivalence-reasoning
X ≃ Y by equiv-1
≃ Z by equiv-2
≃ V by equiv-3


The equivalence constructed in this way is equiv-1 ∘e (equiv-2 ∘e equiv-3), i.e., the equivivalence is associated fully to the right.

Note. In situations where it is important to have precise control over an equivalence or its inverse, it is often better to avoid making use of equivalence reasoning. For example, since many of the entries proving that a map is an equivalence are marked as abstract in agda-unimath, the inverse of an equivalence often does not compute to any map that one might expect the inverse to be. If inverses of equivalences are used in equivalence reasoning, this results in a composed equivalence that also does not compute to any expected underlying map.

Even if a proof by equivalence reasoning is clear to the human reader, constructing equivalences by hand by constructing maps back and forth and two homotopies witnessing that they are mutual inverses is often the most straigtforward solution that gives the best expected computational behavior of the constructed equivalence. In particular, if the underlying map or its inverse are noteworthy maps, it is good practice to define them directly rather than as underlying maps of equivalences constructed by equivalence reasoning.

infixl 1 equivalence-reasoning_
infixl 0 step-equivalence-reasoning

equivalence-reasoning_ :
{l1 : Level} (X : UU l1) → X ≃ X
equivalence-reasoning X = id-equiv

step-equivalence-reasoning :
{l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
(X ≃ Y) → (Z : UU l3) → (Y ≃ Z) → (X ≃ Z)
step-equivalence-reasoning e Z f = f ∘e e

syntax step-equivalence-reasoning e Z f = e ≃ Z by f


### Table of files about function types, composition, and equivalences

ConceptFile
Decidable dependent function typesfoundation.decidable-dependent-function-types
Dependent universal property of equivalencesfoundation.dependent-universal-property-equivalences
Descent for equivalencesfoundation.descent-equivalences
Equivalence extensionalityfoundation.equivalence-extensionality
Equivalence inductionfoundation.equivalence-induction
Equivalencesfoundation.equivalences
Equivalences (foundation-core)foundation-core.equivalences
Families of equivalencesfoundation.families-of-equivalences
Fibered equivalencesfoundation.fibered-equivalences
Function extensionalityfoundation.function-extensionality
Function typesfoundation.function-types
Function types (foundation-core)foundation-core.function-types
Functional correspondencesfoundation.functional-corresponcences
Functoriality of dependent function typesfoundation.functoriality-dependent-function-types
Functoriality of dependent function types (foundation-core)foundation-core.functoriality-dependent-function-types
Functoriality of function typesfoundation.functoriality-function-types
Implicit function typesfoundation.implicit-function-types
Iterating functionsfoundation.iterating-functions
Postcompositionfoundation.postcomposition
Precomposition of dependent functionsfoundation.precomposition-dependent-functions
Precomposition of dependent functions (foundation-core)foundation-core.precomposition-dependent-functions
Precomposition of functionsfoundation.precomposition-functions
Precomposition of functions (foundation-core)foundation-core.precomposition-functions
Precomposition of functions into subuniversesfoundation.precomposition-functions-into-subuniverses
Type arithmetic of dependent function typesfoundation.type-arithmetic-dependent-function-types
Univalence implies function extensionalityfoundation.univalence-implies-function-extensionality
Universal property of equivalencesfoundation.universal-property-equivalences
Weak function extensionalityfoundation.weak-function-extensionality