module Equivalences where

open import Preliminaries

-- Given a map with a left inverse and a right inverse, the left and right inverses are equal.
-- Hence we an isomorphism.
module _ {A B : Set} (f : A → B) (g h : B → A)
  (fg : (b : B) → f (g b) ≡ b) (hf : (a : A) → h (f a) ≡ a) where

  left-inverse-eq-right-inverse : (b : B) → h b ≡ g b
  left-inverse-eq-right-inverse b = ap h (symm (fg b)) • hf (g b)

  iso-of-section-and-retraction : A ≅ B
  iso-of-section-and-retraction .fun = f
  iso-of-section-and-retraction .inv = h
  iso-of-section-and-retraction .inv-fun = hf
  iso-of-section-and-retraction .fun-inv b = ap f (left-inverse-eq-right-inverse b) • fg b

private module _ {A B : Set} (f : A ≅ B) where

  eq-congr' : {a a' : A} → (f .inv (f .fun a) ≡ f .inv (f .fun a')) ≅ a ≡ a'
  eq-congr' = eq-congr (f .inv-fun _) (f .inv-fun _)

  ap-inv : {a a' : A} → f .fun a ≡ f .fun a' → a ≡ a'
  ap-inv = eq-congr' .fun ∘ ap (f .inv)

  ap-inv-ap : {a a' : A} → (p : a ≡ a') → ap-inv (ap (f .fun) p) ≡ p
  ap-inv-ap refl = eq-congr-refl (f .inv-fun _)

module _ {A B : Set} (f : A ≅ B) where

  ap-iso : {a a' : A} →
          (a ≡ a') ≅ (f .fun a ≡ f .fun a')
  ap-iso = inv-iso (iso-of-section-and-retraction (ap-inv f) (ap (f .fun))
        (ap-inv (inv-iso f) ∘ eq-congr' f .inv) (ap-inv-ap f)
        λ p → ap (ap-inv (inv-iso f)) (eq-congr' f .inv-fun _) • ap-inv-ap (inv-iso f) p)

  contr-fib : (b : B) → isContr (fib (f .fun) b)
  contr-fib b = transport (λ b' → isContr (fib (f .fun) b'))
    (contr-congr (Σ-congr-snd λ a → ap-iso) (contr-singleton (f .inv b)))
    (f .fun-inv b)

module _ {A B : Set} {P : B → Set} (f : A ≅ B) (p : (a : A) → P (f .fun a)) where
  abstract
    equiv-ind : (b : B) → P b
    equiv-ind b = transport P (p (f .inv b)) (f .fun-inv b)

    equiv-ind-fun : (a : A) → equiv-ind (f .fun a) ≡ p a
    equiv-ind-fun a = ap (λ t → transport P (p (t .fst)) (t .snd))
                      (isProp-of-isContr (contr-fib f (f .fun a)) _ _)

ap-inl-iso : {A B : Set} {x y : A} → x ≡ y ≅ inl {B = B} x ≡ inl y
ap-inl-iso = ap-iso +-symm ∘ₑ ap-inr-iso

Σ-congr-fst : {A B : Set} {X : B → Set} (e : A ≅ B) → Σ A (λ a → X (e .fun a)) ≅ Σ B X
Σ-congr-fst e .fun t = e .fun (t .fst) , t .snd
Σ-congr-fst e .inv = uncurry (equiv-ind e _,_)
Σ-congr-fst e .inv-fun t = congrFun (equiv-ind-fun e _,_ (t .fst)) (t .snd)
Σ-congr-fst e .fun-inv = uncurry (equiv-ind e λ a x → ap (Σ-congr-fst e .fun) (Σ-congr-fst e .inv-fun _))

Σ-congr : {A B : Set} {X : A → Set} {Y : B → Set} (e : A ≅ B) (f : (a : A) → X a ≅ Y (e .fun a)) →
          Σ A X ≅ Σ B Y
Σ-congr e f = Σ-congr-fst e ∘ₑ Σ-congr-snd f