Martin Escardo, 2012

type ≃ of equivalences 14th September 2017, and rewrote other files to
use them instead, in the spirit of univalent mathematics. The type ≅
is private, and is included for discussion only.

We use Joyal's version of the notion equivalence. The point of the
notion of equivalence is that it is always a univalent proposition,
the data giving a two-sided inverse is not unique in general (although
the inverse is unique in some sense, the data that it is a two-sided
inverse isn't, in the absence of the K axiom).

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module Equivalence where

open import SpartanMLTT

_∼_ : {X Y : U} → (X → Y) → (X → Y) → U
f ∼ g = ∀ x → f x ≡ g x

retraction-section : {X Y : U} → (X → Y) → (Y → X) → U
retraction-section r s = r ∘ s ∼ id

hasTwoSidedInverse : {X Y : U} → (f : X → Y) → U
hasTwoSidedInverse f = Σ \g → retraction-section f g × retraction-section g f

hasSection : {X Y : U} → (f : X → Y) → U
hasSection f = Σ \g → retraction-section f g

hasRetraction : {X Y : U} → (f : X → Y) → U
hasRetraction f = Σ \h → retraction-section h f

isJoyalEquiv : {X Y :  U} → (f : X → Y) → U
isJoyalEquiv f = hasSection f × hasRetraction f

hasTwoSidedInverse-implies-isEquiv : {X Y : U} {f : X → Y} → hasTwoSidedInverse f → isJoyalEquiv f
hasTwoSidedInverse-implies-isEquiv (g , (fg , gf)) = (g , fg) , g , gf

isEquiv-implies-hasTwoSidedInverse : {X Y : U} {f : X → Y} → isJoyalEquiv f → hasTwoSidedInverse f
isEquiv-implies-hasTwoSidedInverse {X} {Y} {f} ((g , fg) , (h , hf)) = g , fg , gf
where
a : (x : X) → g(f x) ≡ h(f(g(f x)))
a x = (hf (g (f x)))⁻¹
b : (x : X) → h(f(g(f x))) ≡ h(f x)
b x = ap h (fg (f x))
gf : (x : X) → g(f x) ≡ x
gf x = a x ∙ b x ∙ hf x

_≃_ : U → U → U
X ≃ Y = Σ \(f : X → Y) → isJoyalEquiv f

infix 19 _≃_

module discussion where
private _≅_ : U → U → U
X ≅ Y = Σ \(f : X → Y) → hasTwoSidedInverse f

private qiso-to-equivalence : {X Y : U} → X ≅ Y → X ≃ Y
qiso-to-equivalence (f , h) = (f , hasTwoSidedInverse-implies-isEquiv h)

private equivalence-to-qiso : {X Y : U} → X ≃ Y → X ≅ Y
equivalence-to-qiso (f , e) = (f , isEquiv-implies-hasTwoSidedInverse e)

\end{code}

This completes the Agda discussion of ≅, and from now on we work with
≃ exclusively. The above two last maps form a section-retraction pair,
with qiso-to-equivalence as the retraction and equivalence-to-qiso as
the section, but we don't prove this here, which follows from the fact
that the type isJoyalEquiv f is a univalent proposition (see the HoTT
Book https://homotopytypetheory.org/book/).

\begin{code}

≃-sym : {X Y : U} → X ≃ Y → Y ≃ X
≃-sym (f , (g , fg) , (h , hf)) = g , (f , gf) , (f , fg)
where
gf : g ∘ f ∼ id
gf = pr₂(pr₂(isEquiv-implies-hasTwoSidedInverse((g , fg) , (h , hf))))

≃-trans : {X Y Z : U} → X ≃ Y → Y ≃ Z → X ≃ Z
≃-trans {X} {Y} {Z} (f , (g , fg) , (h , hf)) (f' , (g' , fg') , (h' , hf'))  =
f' ∘ f , (g ∘ g' , fg'') , (h ∘ h' , hf'')
where
fg'' : (z : Z) → f' (f (g (g' z))) ≡ z
fg'' z =  trans (ap f' (fg (g' z))) (fg' z)
hf'' : (x : X) → h(h'(f'(f x))) ≡ x
hf'' x = trans (ap h (hf' (f x))) (hf x)

Curry-Uncurry : {X : U} {Y : X → U} {Z : (Σ \(x : X) → Y x) → U}
→ ((w : Σ \(x : X) → Y x) → Z w) ≃ ((x : X) (y : Y x) → Z(x , y))
Curry-Uncurry {X} {Y} {Z} = c , (u , cu) , (u , uc)
where
c : ((w : Σ \(x : X) → Y x) → Z w) → ((x : X) (y : Y x) → Z(x , y))
c f x y = f (x , y)
u : ((x : X) (y : Y x) → Z(x , y)) → ((w : Σ \(x : X) → Y x) → Z w)
u g (x , y) = g x y
open import FunExt
cu : ∀ g → c (u g) ≡ g
cu g = funext (λ x → funext (λ y → refl))
uc : ∀ f → u (c f) ≡ f
uc f = funext (λ w → refl)

Σ-≃-congruence : (X : U) (Y Y' : X → U)
→ ((x : X) → Y x ≃ Y' x) → Σ Y ≃ Σ Y'
Σ-≃-congruence X Y Y' φ = (F , (G , FG) , (H , HF))
where
f : (x : X) → Y x → Y' x
f x = pr₁(φ x)
g : (x : X) → Y' x → Y x
g x = pr₁(pr₁(pr₂(φ x)))
fg : (x : X) (y' : Y' x) → f x (g x y') ≡ y'
fg x = pr₂(pr₁(pr₂(φ x)))
h : (x : X) → Y' x → Y x
h x = pr₁(pr₂(pr₂(φ x)))
hf : (x : X) (y : Y x) → h x (f x y) ≡ y
hf x = pr₂(pr₂(pr₂(φ x)))

F : Σ Y → Σ Y'
F (x , y) = x , f x y
G : Σ Y' → Σ Y
G (x , y') = x , (g x y')
H : Σ Y' → Σ Y
H (x , y') = x , h x y'
FG : (w' : Σ Y') → F(G w') ≡ w'
FG (x , y') = Σ-≡' x _ y' (fg x y')
HF : (w : Σ Y) → H(F w) ≡ w
HF (x , y) = Σ-≡' x _ y (hf x y)

Π-congruence : (X : U) (Y Y' : X → U)
→ ((x : X) → Y x ≃ Y' x) → ((x : X) → Y x) ≃ ((x : X) → Y' x)
Π-congruence X Y Y' φ = (F , (G , FG) , (H , HF))
where
f : (x : X) → Y x → Y' x
f x = pr₁(φ x)
g : (x : X) → Y' x → Y x
g x =  pr₁(pr₁(pr₂(φ x)))
fg : (x : X) (y' : Y' x) → f x (g x y') ≡ y'
fg x = pr₂(pr₁(pr₂(φ x)))
h : (x : X) → Y' x → Y x
h x = pr₁(pr₂(pr₂(φ x)))
hf : (x : X) (y : Y x) → h x (f x y) ≡ y
hf x = pr₂(pr₂(pr₂(φ x)))

F : ((x : X) → Y x) → ((x : X) → Y' x)
F = λ z x → pr₁ (φ x) (z x)
G : ((x : X) → Y' x) → (x : X) → Y x
G u x = g x (u x)
H : ((x : X) → Y' x) → (x : X) → Y x
H u' x = h x (u' x)

FG :  (w' : ((x : X) → Y' x)) → F(G w') ≡ w'
FG w' = funext FG'
where
open import FunExt
FG' : (x : X) → F(G w') x ≡ w' x
FG' x = fg x (w' x)

HF : (w : ((x : X) → Y x)) → H(F w) ≡ w
HF w = funext GF'
where
open import FunExt
GF' : (x : X) → H(F w) x ≡ w x
GF' x = hf x (w x)

lemma[𝟙×Y≃Y] : {Y : U} → 𝟙 × Y ≃ Y
lemma[𝟙×Y≃Y] {Y} = (f , (g , fg) , (g , gf))
where
f : 𝟙 × Y → Y
f (* , y) = y
g : Y → 𝟙 × Y
g y = (* , y)
fg : ∀ x → f (g x) ≡ x
fg y = refl
gf : ∀ z → g (f z) ≡ z
gf (* , y) = refl

lemma[X×Y≃Y×X] : {X Y : U} → X × Y ≃ Y × X
lemma[X×Y≃Y×X] {X} {Y} = (f , (g , fg) , (g , gf))
where
f : X × Y → Y × X
f (x , y) = (y , x)
g : Y × X → X × Y
g (y , x) = (x , y)
fg : ∀ z → f (g z) ≡ z
fg z = refl
gf : ∀ t → g (f t) ≡ t
gf t = refl

lemma[Y×𝟙≃Y] : {Y : U} → Y × 𝟙 ≃ Y
lemma[Y×𝟙≃Y] = ≃-trans lemma[X×Y≃Y×X] lemma[𝟙×Y≃Y]

lemma[X≃X'→Y≃Y'→[X×Y]≃[X'×Y']] : {X X' Y Y' : U} → X ≃ X' → Y ≃ Y' → (X × Y) ≃ (X' × Y')
lemma[X≃X'→Y≃Y'→[X×Y]≃[X'×Y']]  {X} {X'} {Y} {Y'} (f , (g , fg) , (h , hf)) (f' , (g' , fg') , (h' , hf')) = (f'' , (g'' , fg'') , (h'' , hf''))
where
f'' : X × Y → X' × Y'
f'' (x , y) = (f x , f' y)
g'' : X' × Y' → X × Y
g'' (x' , y') = (g x' , g' y')
h'' : X' × Y' → X × Y
h'' (x' , y') = (h x' , h' y')
fg'' : ∀ z' → f'' (g'' z') ≡ z'
fg''(x' , y') = ap₂ _,_ lemma₀ lemma₁
where
lemma₀ : f(g x') ≡ x'
lemma₀ = fg x'
lemma₁ : f'(g' y') ≡ y'
lemma₁ = fg' y'
hf'' : ∀ z → h'' (f'' z) ≡ z
hf''(x' , y') = ap₂ _,_ lemma₀ lemma₁
where
lemma₀ : h(f x') ≡ x'
lemma₀ = hf x'
lemma₁ : h'(f' y') ≡ y'
lemma₁ = hf' y'

\end{code}