Martin Escardo, 2012

This file originally had (quasi) isomorphisms ≅ only. We added the
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}