{-# OPTIONS --without-K --safe #-}
module Util.HoTT.Equiv where

open import Util.HoTT.Equiv.Core public

open import Relation.Binary using (Setoid ; IsEquivalence)

open import Util.Data.Product using (map₂)
open import Util.HoTT.HLevel.Core using (IsContr ; IsProp)
open import Util.HoTT.Section
open import Util.HoTT.Singleton using (IsContr-Singleton)
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁻ ; Σ-≡⁺ ; trans-symʳ ; trans-unassoc )


private
  variable
    α β γ : Level
    A B C : Set α


IsIso→HasSection-forth : {f : A → B} → IsIso f → HasSection f
IsIso→HasSection-forth i = record
  { section = i .IsIso.back
  ; isSection = i .IsIso.forth∘back
  }


IsIso→HasSection-back : {f : A → B} → (i : IsIso f) → HasSection (i .IsIso.back)
IsIso→HasSection-back {f = f} i = record
  { section = f
  ; isSection = i .IsIso.back∘forth
  }


IsIso→Injective : {f : A → B} → IsIso f → Injective f
IsIso→Injective f-iso fx≡fy
  = trans (sym (f-iso .IsIso.back∘forth _))
      (trans (cong (f-iso .IsIso.back) fx≡fy)
        (f-iso .IsIso.back∘forth _))


IsEquiv→IsIso : {f : A → B} → IsEquiv f → IsIso f
IsEquiv→IsIso {A = A} {B = B} {forth} equiv = record
  { back = back′ ; back∘forth = back∘forth′ ; forth∘back = forth∘back′ }
  where
  back′ : B → A
  back′ b with equiv b
  ... | (a , _) , _ = a

  back∘forth′ : ∀ x → back′ (forth x) ≡ x
  back∘forth′ a with equiv (forth a)
  ... | (a′ , fortha′≡fortha) , unique = proj₁ (Σ-≡⁻ (unique (a , refl)))

  forth∘back′ : ∀ x → forth (back′ x) ≡ x
  forth∘back′ b with equiv b
  ... | (a , fortha≡b) , _ = fortha≡b


IsEquiv→Injective : {f : A → B} → IsEquiv f → Injective f
IsEquiv→Injective = IsIso→Injective ∘ IsEquiv→IsIso


-- This proof follows Martin Escardó's lecture notes
-- (https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#fibersandequivalences).
IsIso→IsEquiv : {f : A → B} → IsIso f → IsEquiv f
IsIso→IsEquiv {A = A} {B = B} {forth} iso b
  = ◁-pres-IsContr (◁-trans ii iii) IsContr-Singleton
  where
    module I = IsIso iso

    A◁B : A ◁ B
    A◁B = record
      { retraction = I.back
      ; hasSection = IsIso→HasSection-back iso
      }


    i : ∀ b′ → (forth (I.back b′) ≡ b) ◁ (b′ ≡ b)
    i b′ = record
      { retraction = λ b′≡b → trans (I.forth∘back b′) b′≡b
      ; hasSection = record
        { section = λ eq → trans (sym (I.forth∘back b′)) eq
        ; isSection = λ x → let open ≡-Reasoning in
          begin
            trans (I.forth∘back b′) (trans (sym (I.forth∘back b′)) x)
          ≡⟨ trans-unassoc (I.forth∘back b′) ⟩
            trans (trans (I.forth∘back b′) (sym (I.forth∘back b′))) x
          ≡⟨ cong (λ p → trans p x) (trans-symʳ (I.forth∘back b′)) ⟩
            x
          ∎
        }
      }


    ii : ∃[ a ] (forth a ≡ b) ◁ ∃[ b′ ] (forth (I.back b′) ≡ b)
    ii = Σ-◁-reindexing A◁B


    iii : ∃[ b′ ] (forth (I.back b′) ≡ b) ◁ ∃[ b′ ] (b′ ≡ b)
    --                                   aka Singleton b
    iii = Σ-◁ i


≅-refl : A ≅ A
≅-refl .forth x = x
≅-refl .isIso .IsIso.back x = x
≅-refl .isIso .IsIso.forth∘back x = refl
≅-refl .isIso .IsIso.back∘forth x = refl


≅-sym : A ≅ B → B ≅ A
≅-sym A≅B .forth = A≅B .back
≅-sym A≅B .isIso .IsIso.back = A≅B .forth
≅-sym A≅B .isIso .IsIso.back∘forth = A≅B .forth∘back
≅-sym A≅B .isIso .IsIso.forth∘back = A≅B .back∘forth


≅-trans : A ≅ B → B ≅ C → A ≅ C
≅-trans A≅B B≅C .forth = B≅C .forth ∘ A≅B .forth
≅-trans A≅B B≅C .isIso .IsIso.back = A≅B .back ∘ B≅C .back
≅-trans A≅B B≅C .isIso .IsIso.back∘forth x
  = trans (cong (A≅B .back) (B≅C .back∘forth _)) (A≅B .back∘forth _)
≅-trans A≅B B≅C .isIso .IsIso.forth∘back x
  = trans (cong (B≅C .forth) (A≅B .forth∘back _)) (B≅C .forth∘back _)


≅-isEquivalence : IsEquivalence (_≅_ {α})
≅-isEquivalence .IsEquivalence.refl = ≅-refl
≅-isEquivalence .IsEquivalence.sym = ≅-sym
≅-isEquivalence .IsEquivalence.trans = ≅-trans


≅-setoid : ∀ α → Setoid (lsuc α) α
≅-setoid α .Setoid.Carrier = Set α
≅-setoid α .Setoid._≈_ = _≅_
≅-setoid α .Setoid.isEquivalence = ≅-isEquivalence


≅-reflexive : A ≡ B → A ≅ B
≅-reflexive refl = ≅-refl


≡→≅ = ≅-reflexive


≅-Injective : (i : A ≅ B) → Injective (i .forth)
≅-Injective i = IsIso→Injective (i .isIso)


≅→◁ : A ≅ B → A ◁ B
≅→◁ A≅B = record
  { retraction = A≅B .back
  ; hasSection = IsIso→HasSection-back (A≅B .isIso)
  }

≅→▷ : A ≅ B → B ◁ A
≅→▷ A≅B = record
  { retraction = A≅B .forth
  ; hasSection = IsIso→HasSection-forth (A≅B .isIso)
  }


≃→≅ : A ≃ B → A ≅ B
≃→≅ A≃B .forth = A≃B .forth
≃→≅ A≃B .isIso = IsEquiv→IsIso (A≃B .isEquiv)


≅→≃ : A ≅ B → A ≃ B
≅→≃ A≅B .forth = A≅B .forth
≅→≃ A≅B .isEquiv = IsIso→IsEquiv (A≅B .isIso)


id-IsEquiv : IsEquiv (id {A = A})
id-IsEquiv a = (a , refl) , λ { (b , refl) → refl }


≃-refl : A ≃ A
≃-refl = record { forth = id ; isEquiv = id-IsEquiv }


≃-reflexive : A ≡ B → A ≃ B
≃-reflexive refl = ≃-refl


≡→≃ = ≃-reflexive


≃-sym : A ≃ B → B ≃ A
≃-sym = ≅→≃ ∘ ≅-sym ∘ ≃→≅


≃-trans : A ≃ B → B ≃ C → A ≃ C
≃-trans A≃B B≃C = ≅→≃ (≅-trans (≃→≅ A≃B) (≃→≅ B≃C))


≃-isEquivalence : IsEquivalence (_≃_ {α})
≃-isEquivalence .IsEquivalence.refl = ≃-refl
≃-isEquivalence .IsEquivalence.sym = ≃-sym
≃-isEquivalence .IsEquivalence.trans = ≃-trans


≃-setoid : ∀ α → Setoid (lsuc α) α
≃-setoid α .Setoid.Carrier = Set α
≃-setoid α .Setoid._≈_ = _≃_
≃-setoid α .Setoid.isEquivalence = ≃-isEquivalence


≃-Injective : (e : A ≃ B) → Injective (e .forth)
≃-Injective = ≅-Injective ∘ ≃→≅


≃→◁ : A ≃ B → A ◁ B
≃→◁ = ≅→◁ ∘ ≃→≅


≃→▷ : A ≃ B → B ◁ A
≃→▷ = ≅→▷ ∘ ≃→≅


-- Special cases of ≃-pres-IsOfHLevel (in Util.HoTT.HLevel), but proven
-- directly. This means that A and B can be at different levels.
≅-pres-IsContr : A ≅ B → IsContr A → IsContr B
≅-pres-IsContr A≅B (a , canon) = A≅B .forth a , λ a′
  → trans (cong (A≅B .forth) (canon (A≅B .back a′))) (A≅B .forth∘back _)


≃-pres-IsContr : A ≃ B → IsContr A → IsContr B
≃-pres-IsContr A≃B = ≅-pres-IsContr (≃→≅ A≃B)


≅-pres-IsProp : A ≅ B → IsProp A → IsProp B
≅-pres-IsProp A≅B A-prop x y
  = trans (sym (A≅B .forth∘back x))
      (sym (trans (sym (A≅B .forth∘back y)) (cong (A≅B .forth) (A-prop _ _))))


≃-pres-IsProp : A ≃ B → IsProp A → IsProp B
≃-pres-IsProp A≃B = ≅-pres-IsProp (≃→≅ A≃B)


Σ-≅⁺ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (∀ a → B a ≅ C a)
  → Σ A B ≅ Σ A C
Σ-≅⁺ eq = record
  { forth = λ { (a , b) → a , eq a .forth b }
  ; isIso = record
    { back = λ { (a , c) → a , eq a .back c }
    ; back∘forth = λ { (a , b) → Σ-≡⁺ (refl , eq a .back∘forth b) }
    ; forth∘back = λ { (a , c) → Σ-≡⁺ (refl , eq a .forth∘back c) }
    }
  }


Σ-≃⁺ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (∀ a → B a ≃ C a)
  → Σ A B ≃ Σ A C
Σ-≃⁺ eq = ≅→≃ (Σ-≅⁺ λ a → ≃→≅ (eq a))


map₂-fiber-≃ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (f : ∀ a → B a → C a)
  → ∀ a (c : C a)
  → ∃[ b ] (f a b ≡ c) ≃ ∃[ p ] (map₂ f p ≡ (a , c))
map₂-fiber-≃ f a c = ≅→≃ record
  { forth = λ { (b , refl) → (a , b) , refl }
  ; isIso = record
    { back = λ { ((.a , b) , refl) → b , refl }
    ; back∘forth = λ { (b , refl) → refl }
    ; forth∘back = λ { ((.a , b) , refl) → refl }
    }
  }


IsEquiv-map₂-f→IsEquiv-f : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (f : ∀ a → B a → C a)
  → IsEquiv (map₂ f)
  → ∀ a → IsEquiv (f a)
IsEquiv-map₂-f→IsEquiv-f {A = A} {B} {C} f equiv a c
  = ≃-pres-IsContr (≃-sym (map₂-fiber-≃ f a c)) (equiv (a , c))


sym-≅ : {x y : A} → (x ≡ y) ≅ (y ≡ x)
sym-≅ = record
  { forth = sym
  ; isIso = record
    { back = sym
    ; back∘forth = λ { refl → refl }
    ; forth∘back = λ { refl → refl }
    }
  }


sym-≃ : {x y : A} → (x ≡ y) ≃ (y ≡ x)
sym-≃ = ≅→≃ sym-≅


IsContr→IsIso : IsContr A → IsContr B → (f : A → B) → IsIso f
IsContr→IsIso (a , a-uniq) (b , b-uniq) f = record
  { back = λ _ → a
  ; back∘forth = λ _ → a-uniq _
  ; forth∘back = λ b′ → trans (sym (b-uniq (f a))) (b-uniq b′)
  }


IsContr→IsEquiv : IsContr A → IsContr B → (f : A → B) → IsEquiv f
IsContr→IsEquiv A-contr B-contr f
  = IsIso→IsEquiv (IsContr→IsIso A-contr B-contr f)


proj₁-IsIso : {A : Set α} {B : A → Set β}
  → (∀ a → IsContr (B a))
  → IsIso (proj₁ {A = A} {B})
proj₁-IsIso B-contr = record
  { back = λ a → (a , B-contr a .proj₁)
  ; back∘forth = λ { (a , b) → Σ-≡⁺ (refl , (B-contr a .proj₂ b)) }
  ; forth∘back = λ _ → refl
  }


proj₁-IsEquiv : {A : Set α} {B : A → Set β}
  → (∀ a → IsContr (B a))
  → IsEquiv (proj₁ {A = A} {B})
proj₁-IsEquiv B-contr = IsIso→IsEquiv (proj₁-IsIso B-contr)


Π-distr-Σ-≅ : (A : Set α) (B : A → Set β) (C : ∀ a → B a → Set γ)
  → (∀ a → Σ[ b ∈ B a ] (C a b))
  ≅ (Σ[ f ∈ (∀ a → B a) ] (∀ a → C a (f a)))
Π-distr-Σ-≅ A B C = record
  { forth = λ f → (λ a → f a .proj₁) , (λ a → f a .proj₂)
  ; isIso = record
    { back = λ { (f , g) → λ a → f a , g a }
    ; back∘forth = λ _ → refl
    ; forth∘back = λ _ → refl
    }
  }