{-# OPTIONS --without-K --rewriting #-}

open import lib.Base
open import lib.NType
open import lib.PathFunctor
open import lib.PathGroupoid
open import lib.Function

module lib.Equivalence where

{-
We use the half-adjoint definition of equivalences (but this fact should be
invisible to the user of the library). The constructor of the type of
equivalences is [equiv], it takes two maps and the two proofs that the composites
are equal: [equiv to from to-from from-to]

The type of equivalences between two types [A] and [B] can be written either
[A ≃ B] or [Equiv A B].

Given an equivalence [e] : [A ≃ B], you can extract the two maps as follows:
[–> e] : [A → B] and [<– e] : [B → A] (the dash is an en dash)
The proofs that the composites are the identities are [<–-inv-l] and [<–-inv-r].

The identity equivalence on [A] is [ide A], the composition of two equivalences
is [_∘e_] (function composition order) and the inverse of an equivalence is [_⁻¹]
-}

{- These lemmas are here because lib.Path is not available at this point.
   Otherwise they are just combinations of [↓-='-out] and [apd]. -}

private
  htpy-natural :  {i j} {A : Type i} {B : Type j} {x y : A} {f g : A  B}
    (p :  x  (f x == g x)) (q : x == y)  ap f q  p y == p x  ap g q
  htpy-natural p idp = ! (∙-unit-r _)

  htpy-natural-app=idf :  {i} {A : Type i} {f : A  A}
    (p :  (x : A)  f x == x)  (∀ x  ap f (p x) == p (f x))
  htpy-natural-app=idf {f = f} p x = anti-whisker-right (p x) $
    htpy-natural p (p x)  ap (p (f x) ∙_) (ap-idf (p x))


module _ {i} {j} {A : Type i} {B : Type j} where

  record is-equiv (f : A  B) : Type (lmax i j)
    where
    field
      g : B  A
      f-g : (b : B)  f (g b) == b
      g-f : (a : A)  g (f a) == a
      adj : (a : A)  ap f (g-f a) == f-g (f a)

    abstract
      adj' : (b : B)  ap g (f-g b) == g-f (g b)
      adj' b = anti-whisker-left (ap g (f-g (f (g b)))) $ ! $
        ap g (f-g (f (g b)))  g-f (g b)
          =⟨ ! $ htpy-natural-app=idf f-g b |in-ctx  p  ap g p  g-f (g b)) 
        ap g (ap (f  g) (f-g b))  g-f (g b)
          =⟨ ! $ ap-∘ g (f  g) (f-g b) |in-ctx  p  p  g-f (g b)) 
        ap (g  f  g) (f-g b)  g-f (g b)
          =⟨ htpy-natural (g-f  g) (f-g b) 
        g-f (g (f (g b)))  ap g (f-g b)
          =⟨ ! $ htpy-natural-app=idf g-f (g b) |in-ctx  p  p  ap g (f-g b)) 
        ap (g  f) (g-f (g b))  ap g (f-g b)
          =⟨ ap-∘ g f (g-f (g b)) |in-ctx  p  p  ap g (f-g b)) 
        ap g (ap f (g-f (g b)))  ap g (f-g b)
          =⟨ adj (g b) |in-ctx  p  ap g p  ap g (f-g b)) 
        ap g (f-g (f (g b)))  ap g (f-g b)
          =∎


  {-
  In order to prove that something is an equivalence, you have to give an inverse
  and a proof that it’s an inverse (you don’t need the adj part).
  [is-eq] is a very, very bad name.
  -}
  is-eq : (f : A  B)
    (g : B  A) (f-g : (b : B)  f (g b) == b)
    (g-f : (a : A)  g (f a) == a)  is-equiv f
  is-eq f g f-g g-f =
   record {g = g; f-g = f-g'; g-f = g-f; adj = adj} where
    abstract
     f-g' : (b : B)  f (g b) == b
     f-g' b = ! (ap (f  g) (f-g b))  ap f (g-f (g b))  f-g b

     adj : (a : A)  ap f (g-f a) == f-g' (f a)
     adj a =
      ap f (g-f a)
        =⟨ ! (!-inv-l (ap (f  g) (f-g (f a)))) |in-ctx  q  q  ap f (g-f a)) 
      (! (ap (f  g) (f-g (f a)))  ap (f  g) (f-g (f a)))  ap f (g-f a)
        =⟨ ∙-assoc (! (ap (f  g) (f-g (f a)))) (ap (f  g) (f-g (f a))) _ 
      ! (ap (f  g) (f-g (f a)))  ap (f  g) (f-g (f a))  ap f (g-f a)
        =⟨ lemma |in-ctx  q  ! (ap (f  g) (f-g (f a)))  q) 
      ! (ap (f  g) (f-g (f a)))  ap f (g-f (g (f a)))  f-g (f a) =∎
      where
      lemma : ap (f  g) (f-g (f a))  ap f (g-f a)
           == ap f (g-f (g (f a)))  f-g (f a)
      lemma =
        ap (f  g) (f-g (f a))  ap f (g-f a)
          =⟨ htpy-natural-app=idf f-g (f a) |in-ctx  q  q  ap f (g-f a)) 
        f-g (f (g (f a)))  ap f (g-f a)
          =⟨ ! (ap-idf (ap f (g-f a))) |in-ctx  q  f-g (f (g (f a)))  q) 
        f-g (f (g (f a)))  ap (idf B) (ap f (g-f a))
          =⟨ ! (htpy-natural f-g (ap f (g-f a))) 
        ap (f  g) (ap f (g-f a))  f-g (f a)
          =⟨ ap-∘ f g (ap f (g-f a)) |in-ctx  q  q  f-g (f a)) 
        ap f (ap g (ap f (g-f a)))  f-g (f a)
          =⟨ ∘-ap g f (g-f a)  htpy-natural-app=idf g-f a
             |in-ctx  q  ap f q  f-g (f a)) 
        ap f (g-f (g (f a)))  f-g (f a) =∎

infix 30 _≃_

_≃_ :  {i j} (A : Type i) (B : Type j)  Type (lmax i j)
A  B = Σ (A  B) is-equiv

Equiv = _≃_

module _ {i} {j} {A : Type i} {B : Type j} where

  equiv : (f : A  B) (g : B  A) (f-g : (b : B)  f (g b) == b)
          (g-f : (a : A)  g (f a) == a)  A  B
  equiv f g f-g g-f = (f , is-eq f g f-g g-f)

  –> : (e : A  B)  (A  B)
  –> e = fst e

  <– : (e : A  B)  (B  A)
  <– e = is-equiv.g (snd e)

  <–-inv-l : (e : A  B) (a : A)
     (<– e (–> e a) == a)
  <–-inv-l e a = is-equiv.g-f (snd e) a

  <–-inv-r : (e : A  B) (b : B)
     (–> e (<– e b) == b)
  <–-inv-r e b = is-equiv.f-g (snd e) b

  <–-inv-adj : (e : A  B) (a : A)
     ap (–> e) (<–-inv-l e a) == <–-inv-r e (–> e a)
  <–-inv-adj e a = is-equiv.adj (snd e) a

  <–-inv-adj' : (e : A  B) (b : B)
     ap (<– e) (<–-inv-r e b) == <–-inv-l e (<– e b)
  <–-inv-adj' e b = is-equiv.adj' (snd e) b

  -- Equivalences are "injective"
  –>-is-inj : (e : A  B)  is-inj (–> e)
  –>-is-inj e x y p = ! (<–-inv-l e x)  ap (<– e) p  <–-inv-l e y

  –>-≠ : (e : A  B)  {a₀ a₁ : A}  a₀  a₁  –> e a₀  –> e a₁
  –>-≠ e {a₀} {a₁} neq = neq  –>-is-inj e a₀ a₁

  equiv-is-inj : {f : A  B}  is-equiv f  is-inj f
  equiv-is-inj ise = –>-is-inj (_ , ise)

idf-is-equiv :  {i} (A : Type i)  is-equiv (idf A)
idf-is-equiv A = record {g = idf A; f-g =  _  idp); g-f =  _  idp); adj =  _  idp)}

ide :  {i} (A : Type i)  A  A
ide A = idf A , idf-is-equiv A

transport-equiv :  {i j} {A : Type i} (B : A  Type j) {x y : A} (p : x == y)
   (B x  B y)
transport-equiv B idp = ide _

infixr 80 _∘e_
infixr 80 _∘ise_

_∘e_ :  {i j k} {A : Type i} {B : Type j} {C : Type k}
   B  C  A  B  A  C
e1 ∘e e2 = (–> e1  –> e2) , record {g = (<– e2  <– e1); M} where
  module M where
    f = –> e1  –> e2
    g = <– e2  <– e1
    abstract
      f-g :  c  f (g c) == c
      f-g c = ap (–> e1) (<–-inv-r e2 (<– e1 c))  <–-inv-r e1 c
      g-f :  a  g (f a) == a
      g-f a = ap (<– e2) (<–-inv-l e1 (–> e2 a))  <–-inv-l e2 a
      adj :  a  ap f (g-f a) == f-g (f a)
      adj a =
        ap (–> e1  –> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a))  <–-inv-l e2 a)
            =⟨ ap-∘ (–> e1) (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a))  <–-inv-l e2 a) 
        ap (–> e1) (ap (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a))  <–-inv-l e2 a))
            =⟨ ap-∙ (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a))) (<–-inv-l e2 a)  |in-ctx ap (–> e1) 
        ap (–> e1) (ap (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a)))  ap (–> e2) (<–-inv-l e2 a))
            =⟨ ! (ap-∘ (–> e2) (<– e2) (<–-inv-l e1 (–> e2 a))) ∙2 <–-inv-adj e2 a |in-ctx ap (–> e1) 
        ap (–> e1) (ap (–> e2  <– e2) (<–-inv-l e1 (–> e2 a))  <–-inv-r e2 (–> e2 a))
            =⟨ htpy-natural (<–-inv-r e2) (<–-inv-l e1 (–> e2 a))    |in-ctx ap (–> e1) 
        ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1  –> e2) a))  ap  z  z) (<–-inv-l e1 (–> e2 a)))
            =⟨ <–-inv-r e2 (<– e1 ((–> e1  –> e2) a)) ∙ₗ ap-idf (<–-inv-l e1 (–> e2 a)) |in-ctx ap (–> e1) 
        ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1  –> e2) a))  <–-inv-l e1 (–> e2 a))
            =⟨ ap-∙ (–> e1) (<–-inv-r e2 (<– e1 ((–> e1  –> e2) a))) (<–-inv-l e1 (–> e2 a)) 
        ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1  –> e2) a)))  ap (–> e1) (<–-inv-l e1 (–> e2 a))
            =⟨  ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1  –> e2) a))) ∙ₗ (<–-inv-adj e1 (–> e2 a)) 
        ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1  –> e2) a)))  <–-inv-r e1 ((–> e1  –> e2) a)
            =∎

_∘ise_ :  {i j k} {A : Type i} {B : Type j} {C : Type k}
  {f : A  B} {g : B  C}
   is-equiv g  is-equiv f  is-equiv (g  f)
i1 ∘ise i2 = snd ((_ , i1) ∘e (_ , i2))

is-equiv-inverse :  {i j} {A : Type i} {B : Type j} {f : A  B}
   (f-is-equiv : is-equiv f)  is-equiv (is-equiv.g f-is-equiv)
is-equiv-inverse {f = g} ise = record { g = _ ; M } where
  module M where
    f = is-equiv.g ise
    abstract
      f-g :  b  f (g b) == b
      f-g = is-equiv.g-f ise
      g-f :  a  g (f a) == a
      g-f = is-equiv.f-g ise
      adj :  a  ap f (g-f a) == f-g (f a)
      adj = is-equiv.adj' ise

infix 120 _⁻¹
_⁻¹ :  {i j} {A : Type i} {B : Type j}  (A  B)  (B  A)
(_ , ise) ⁻¹ = (is-equiv.g ise , is-equiv-inverse ise)

{- Equational reasoning for equivalences -}
infix 15 _≃∎
infixr 10 _≃⟨_⟩_

_≃⟨_⟩_ :  {i j k} (A : Type i) {B : Type j} {C : Type k}  A  B  B  C  A  C
A ≃⟨ u  v = v ∘e u

_≃∎ :  {i} (A : Type i)  A  A
_≃∎ = ide


{- lifting is an equivalence -}
lower-equiv :  {i j} {A : Type i}  Lift {j = j} A  A
lower-equiv = equiv lower lift  _  idp)  _  idp)

{- Any contractible type is equivalent to (all liftings of) the unit type -}
module _ {i} {A : Type i} (h : is-contr A) where
  contr-equiv-Unit : A  Unit
  contr-equiv-Unit = equiv  _  unit)  _  contr-center h)  _  idp) (contr-path h)

  contr-equiv-LiftUnit :  {j}  A  Lift {j = j} Unit
  contr-equiv-LiftUnit = lower-equiv ⁻¹ ∘e contr-equiv-Unit


{- An equivalence induces an equivalence on the path spaces -}
module _ {i j} {A : Type i} {B : Type j} where

  private
    abstract
      left-inverse : (e : A  B) {x y : A} (p : x == y)
         –>-is-inj e _ _ (ap (–> e) p) == p
      left-inverse e idp = !-inv-l (<–-inv-l e _)

      right-inverse : (e : A  B) {x y : A} (p : –> e x == –> e y)
         ap (–> e) (–>-is-inj e _ _ p) == p
      right-inverse e {x} {y} p =
        ap f (! (g-f x)  ap g p  (g-f y))
          =⟨ ap-∙ f (! (g-f x)) (ap g p  (g-f y)) 
        ap f (! (g-f x))  ap f (ap g p  (g-f y))
          =⟨ ap-∙ f (ap g p) (g-f y) |in-ctx  q   ap f (! (g-f x))  q) 
        ap f (! (g-f x))  ap f (ap g p)  ap f (g-f y)
          =⟨ ∘-ap f g p |in-ctx  q  ap f (! (g-f x))  q  ap f (g-f y)) 
        ap f (! (g-f x))  ap (f  g) p  ap f (g-f y)
          =⟨ adj y |in-ctx  q   ap f (! (g-f x))  ap (f  g) p  q) 
        ap f (! (g-f x))  ap (f  g) p  (f-g (f y))
          =⟨ ap-! f (g-f x) |in-ctx  q  q  ap (f  g) p  (f-g (f y))) 
        ! (ap f (g-f x))  ap (f  g) p  (f-g (f y))
          =⟨ adj x |in-ctx  q   ! q  ap (f  g) p  (f-g (f y))) 
        ! (f-g (f x))  ap (f  g) p  (f-g (f y))
          =⟨ htpy-natural f-g p |in-ctx  q   ! (f-g (f x))  q) 
        ! (f-g (f x))  (f-g (f x))  ap (idf B) p
          =⟨ ! (∙-assoc (! (f-g (f x))) (f-g (f x)) (ap (idf B) p))
              ap  q  q  ap (idf B) p) (!-inv-l (f-g (f x)))  ap-idf p 
        p =∎
        where f : A  B
              f = fst e

              open is-equiv (snd e)

  ap-is-equiv : {f : A  B}  is-equiv f
     (x y : A)  is-equiv (ap f :> (x == y  f x == f y))
  ap-is-equiv {f} e x y =
    is-eq (ap f) (equiv-is-inj e _ _) (right-inverse (_ , e)) (left-inverse (_ , e))

  ap-equiv : (e : A  B) (x y : A)  (x == y)  (–> e x == –> e y)
  ap-equiv e x y = _ , ap-is-equiv (snd e) x y

{- Equivalent types have the same truncation level -}
abstract
  equiv-preserves-level :  {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A  B)
    {{_ : has-level n A}}  has-level n B
  equiv-preserves-level {n = ⟨-2⟩} e {{p}} =
    has-level-in (–> e (contr-center p) ,  y  ap (–> e) (contr-path p _)  <–-inv-r e y))
  equiv-preserves-level {n = S n} e {{c}} = has-level-in  x y 
    equiv-preserves-level (ap-equiv (e ⁻¹) x y ⁻¹) {{has-level-apply c (<– e x) (<– e y)}})

{- This is a collection of type equivalences involving basic type formers.
   We exclude Empty since Π₁-Empty requires λ=.
-}
module _ {j} {B : Unit  Type j} where
  Σ₁-Unit : Σ Unit B  B unit
  Σ₁-Unit = equiv  {(unit , b)  b})  b  (unit , b))  _  idp)  _  idp)

  Π₁-Unit : Π Unit B  B unit
  Π₁-Unit = equiv  f  f unit)  b _  b)  _  idp)  _  idp)

module _ {i} {A : Type i} where
  Σ₂-Unit : Σ A  _  Unit)  A
  Σ₂-Unit = equiv fst  a  (a , unit))  _  idp)  _  idp)

  Π₂-Unit : Π A  _  Unit)  Unit
  Π₂-Unit = equiv  _  unit)  _ _  unit)  _  idp)  _  idp)

module _ {i j k} {A : Type i} {B : A  Type j} {C : (a : A)  B a  Type k} where
  Σ-assoc : Σ (Σ A B) (uncurry C)  Σ A  a  Σ (B a) (C a))
  Σ-assoc = equiv  {((a , b) , c)  (a , (b , c))})
                   {(a , (b , c))  ((a , b) , c)})  _  idp)  _  idp)

  curry-equiv : Π (Σ A B) (uncurry C)  Π A  a  Π (B a) (C a))
  curry-equiv = equiv curry uncurry  _  idp)  _  idp)

  {- The type-theoretic axiom of choice -}
  choice : Π A  a  Σ (B a)  b  C a b))  Σ (Π A B)  g  Π A  a  C a (g a)))
  choice = equiv f g  _  idp)  _  idp)
    where f = λ c  ((λ a  fst (c a)) ,  a  snd (c a)))
          g = λ d   a  (fst d a , snd d a))

∼-preserves-equiv :  {i j} {A : Type i} {B : Type j} {f₀ f₁ : A  B}
   f₀  f₁  is-equiv f₀  is-equiv f₁
∼-preserves-equiv homotopy f-ise =
  is-eq _ g  b  ! (homotopy (g b))  f-g b)  a  ap g (! (homotopy a))  g-f a)
  where open is-equiv f-ise

{-
Pointed equivalences
-}

infix 30 _⊙≃_
_⊙≃_ :  {i j}  Ptd i  Ptd j  Type (lmax i j)
X ⊙≃ Y = Σ (X ⊙→ Y)  {(f , _)  is-equiv f})

≃-to-⊙≃ :  {i j} {X : Ptd i} {Y : Ptd j}
  (e : de⊙ X  de⊙ Y) (p : –> e (pt X) == pt Y)
   X ⊙≃ Y
≃-to-⊙≃ (f , ie) p = ((f , p) , ie)

⊙ide :  {i} (X : Ptd i)  (X ⊙≃ X)
⊙ide X = ⊙idf X , idf-is-equiv (de⊙ X)

infixr 80 _⊙∘e_
_⊙∘e_ :  {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙≃ Z) (f : X ⊙≃ Y)  X ⊙≃ Z
(g , g-eq) ⊙∘e (f , f-eq) = (g ⊙∘ f , g-eq ∘ise f-eq)

infix 15 _⊙≃∎
infixr 10 _⊙≃⟨_⟩_

_⊙≃⟨_⟩_ :  {i j k} (X : Ptd i) {Y : Ptd j} {Z : Ptd k}
   X ⊙≃ Y  Y ⊙≃ Z  X ⊙≃ Z
X ⊙≃⟨ u  v = v ⊙∘e u

_⊙≃∎ :  {i} (X : Ptd i)  X ⊙≃ X
_⊙≃∎ = ⊙ide

is-cs-equiv :  {i₀ i₁ j₀ j₁}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {f₀ : A₀  B₀} {f₁ : A₁  B₁} {hA : A₀  A₁} {hB : B₀  B₁}
   CommSquare f₀ f₁ hA hB  Type (lmax (lmax i₀ i₁) (lmax j₀ j₁))
is-cs-equiv {hA = hA} {hB} _ = Σ (is-equiv hA)  _  is-equiv hB)

CommSquareEquiv :  {i₀ i₁ j₀ j₁}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  (f₀ : A₀  B₀) (f₁ : A₁  B₁) (hA : A₀  A₁) (hB : B₀  B₁)
   Type (lmax (lmax i₀ i₁) (lmax j₀ j₁))
CommSquareEquiv f₀ f₁ hA hB = Σ (CommSquare f₀ f₁ hA hB) is-cs-equiv

is-⊙cs-equiv :  {i₀ i₁ j₀ j₁}
  {X₀ : Ptd i₀} {X₁ : Ptd i₁} {Y₀ : Ptd j₀} {Y₁ : Ptd j₁}
  {f₀ : X₀ ⊙→ Y₀} {f₁ : X₁ ⊙→ Y₁} {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
   ⊙CommSquare f₀ f₁ hX hY  Type (lmax (lmax i₀ i₁) (lmax j₀ j₁))
is-⊙cs-equiv {hX = hX} {hY} _ = Σ (is-equiv (fst hX))  _  is-equiv (fst hY))

⊙CommSquareEquiv :  {i₀ i₁ j₀ j₁}
  {X₀ : Ptd i₀} {X₁ : Ptd i₁} {Y₀ : Ptd j₀} {Y₁ : Ptd j₁}
  (f₀ : X₀ ⊙→ Y₀) (f₁ : X₁ ⊙→ Y₁) (hX : X₀ ⊙→ X₁) (hY : Y₀ ⊙→ Y₁)
   Type (lmax (lmax i₀ i₁) (lmax j₀ j₁))
⊙CommSquareEquiv f₀ f₁ hX hY = Σ (⊙CommSquare f₀ f₁ hX hY) is-⊙cs-equiv