{-# OPTIONS --without-K #-}
open import function.extensionality.core

module hott.weak-equivalence.alternative where

open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.extensionality.dependent
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.utils
open import hott.hlevel.core
open import hott.weak-equivalence.core
open import hott.univalence

private
  module Properties {i j}{X : Set i}{Y : Set j} where
    open ≅-Reasoning

    private
      A : (f : X → Y)(g : Y → X) → Set _
      A f g = (x : X) → g (f x) ≡ x

      B : (f : X → Y)(g : Y → X) → Set _
      B f g = (y : Y) → f (g y) ≡ y

      GB : (f : X → Y) → Set _
      GB f = Σ (Y → X) (B f)

      Φ : (f : X → Y)(g : Y → X) → Set _
      Φ f g = (y : Y)(x : X) → f x ≡ y → g y ≡ x

      Ψ : (f : X → Y)(g : Y → X)(β : B f g)(φ : Φ f g) → Set _
      Ψ f g β φ = (y : Y)(x : X)(p : f x ≡ y) → cong f (φ y x p) ⊚ p ≡ β y

      W : Set _
      W = Σ (X → Y) λ f
        → Σ (GB f) λ { (g , β)
        → Σ (Φ f g) (Ψ f g β) }

      -- isomorphism inside Π
      Π-iso : ∀ {i j j'} {X : Set i}
              {Y : X → Set j}{Y' : X → Set j'}
            → ((x : X) → Y x ≅ Y' x)
            → ((x : X) → Y x)
            ≅ ((x : X) → Y' x)
      Π-iso = Π-cong-iso ext' refl≅

      -- flipped transitivity of isomorphism
      -- makes some proofs easier to read
      _⋆_ : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
          → Y ≅ Z → X ≅ Y → X ≅ Z
      isom ⋆ isom' = trans≅ isom' isom

      -- inverse image contractible ≅ (φ , ψ)
      contr-split : (f : X → Y)(g : Y → X)(β : B f g)
                  → ((y : Y)(x : f ⁻¹ y) → (g y , β y) ≡ x)
                  ≅ Σ (Φ f g) (Ψ f g β)
      contr-split f g β = begin
          ((y : Y)(x : f ⁻¹ y) → (g y , β y) ≡ x)
        ≅⟨ (Π-iso λ y → curry-iso (λ x p → (g y , β y) ≡ (x , p))) ⟩
          ((y : Y)(x : X)(p : f x ≡ y) → (g y , β y) ≡ (x , p))
        ≅⟨ (Π-iso λ y → Π-iso λ x → Π-iso λ p
         → sym≅ (Σ-split-iso {b = β y}{b' = p})) ⟩
          ((y : Y)(x : X)(p : f x ≡ y) → Σ (g y ≡ x) λ q
                → subst (λ x → f x ≡ y) q (β y) ≡ p)
        ≅⟨ (ΠΣ-swap-iso ⋆ Π-iso λ y
         → ΠΣ-swap-iso ⋆ Π-iso λ x
         → ΠΣ-swap-iso {Z = λ p q → subst (λ x → f x ≡ y) q (β y) ≡ p}) ⟩
         ( Σ (Φ f g) λ φ
         → (y : Y)(x : X)(p : f x ≡ y)
                → subst (λ x → f x ≡ y) (φ y x p) (β y) ≡ p )
        ≅⟨ (Σ-cong-iso refl≅ λ φ
         → Π-iso λ y → Π-iso λ x → Π-iso λ p
         → lem f g β φ y x p) ⟩
          Σ (Φ f g) (Ψ f g β)
        ∎
        where
          lem : (f : X → Y)(g : Y → X)(β : (y : Y) → f (g y) ≡ y)
                (φ : (y : Y)(x : X) → f x ≡ y → g y ≡ x)
              → (y : Y)(x : X)(p : f x ≡ y)
              → (subst (λ x → f x ≡ y) (φ y x p) (β y) ≡ p)
              ≅ (cong f (φ y x p) ⊚ p ≡ β y)
          lem f g β φ y x p = begin
              subst (λ x → f x ≡ y) (φ y x p) (β y) ≡ p
            ≡⟨ cong (λ z → z ≡ p)
                    ( subst-naturality (λ x → x ≡ y) f (φ y x p) (β y)
                    ⊚ subst-eq (cong f (φ y x p)) (β y) ) ⟩
              sym (cong f (φ y x p)) ⊚ β y ≡ p
            ≅⟨ sym≅ (move-≡-iso (cong f (φ y x p)) p (β y)) ⟩
              cong f (φ y x p) ⊚ p ≡ β y
            ∎

      -- weak equivalence ≅ (f , g , β , φ , ψ)
      weak-equiv-split : (X ≈ Y) ≅ W
      weak-equiv-split =
        Σ-cong-iso refl≅ (λ f → begin
            weak-equiv f
          ≅⟨ ΠΣ-swap-iso ⟩
            Σ ((y : Y) → f ⁻¹ y) (λ { gβ
            → (y : Y)(x : f ⁻¹ y) → gβ y ≡ x })
          ≅⟨ Σ-cong-iso ΠΣ-swap-iso (λ _ → refl≅) ⟩
            ( Σ (GB f) λ { (g , β)
            → (y : Y)(x : f ⁻¹ y) → (g y , β y) ≡ x } )
          ≅⟨ Σ-cong-iso refl≅ (λ { (g , β) → contr-split f g β }) ⟩
            ( Σ (GB f) λ { (g , β)
            → Σ (Φ f g) (Ψ f g β) } )
          ∎ )

    -- weak-equivalence ≅ coherent isomorphism
    ≈⇔≅' : (X ≈ Y) ≅ (X ≅' Y)
    ≈⇔≅' = begin
        X ≈ Y
      ≅⟨ weak-equiv-split ⟩
        W
      ≅⟨ Σ-cong-iso refl≅ (λ f
         → Σ-cong-iso refl≅ λ { (g , K)
         → Σ-cong-iso {Y = Ψ f g K}
                       (φ≅H f g)
                       (λ H → ψ≅γ f g H K) }) ⟩
        ( Σ (X → Y) λ f
        → Σ (GB f) λ { (g , K)
        → Σ (A f g) λ H
        → coherent (iso f g H K) } )
      ≅⟨ iso (λ { (f , (g , K) , H , γ) → iso f g H K , γ })
             (λ { (iso f g H K , γ) → (f , (g , K) , H , γ) })
             (λ _ → refl) (λ _ → refl) ⟩
        X ≅' Y
      ∎
      where
        Ψ' : (f : X → Y)(g : Y → X)(K : B f g)(H : A f g) → Set _
        Ψ' f g K H = ((y : Y)(x : X)(p : f x ≡ y)
                   → cong f (sym (cong g p) ⊚ H x) ⊚ p ≡ K y)

        φ≅H : (f : X → Y)(g : Y → X) → Φ f g ≅ A f g
        φ≅H f g = record
          { to = λ φ x → φ (f x) x refl
          ; from = λ H y x p → sym (cong g p) ⊚ H x 
          ; iso₁ = λ φ → ext' λ y → ext' λ x → ext' λ p → lem φ y x p
          ; iso₂ = λ H → refl }
          where
            lem : (φ : (y : Y)(x : X) → f x ≡ y → g y ≡ x)
                → (y : Y)(x : X)(p : f x ≡ y)
                → sym (cong g p) ⊚ φ (f x) x refl ≡ φ y x p
            lem φ .(f x) x refl = refl

        ψ≅γ : (f : X → Y)(g : Y → X)(H : A f g)(K : B f g)
            → Ψ' f g K H ≅ coherent (iso f g H K)
        ψ≅γ f g H K = record
          { to = to
          ; from = from
          ; iso₁ = λ ψ → ext' λ y → ext' λ x → ext' λ p → lem₁ ψ y x p
          ; iso₂ = λ γ → ext' λ x → lem₂ γ x }
          where
            to : Ψ' f g K H → coherent (iso f g H K)
            to ψ x = sym (left-unit _) ⊚ ψ (f x) x refl

            from : coherent (iso f g H K) → Ψ' f g K H
            from γ .(f x) x refl = left-unit _ ⊚ γ x

            lem₁ : (ψ : Ψ' f g K H)(y : Y)(x : X)(p : f x ≡ y)
                → from (to ψ) y x p ≡ ψ y x p
            lem₁ φ .(f x) x refl =
              J (λ u v q → (z : f (g (f x)) ≡ f x)
                            (r : u ≡ z)
                         → q ⊚ (sym q ⊚ r) ≡ r)
                (λ u z r → refl) _ _
                (left-unit (cong f (H x))) _
                (φ (f x) x refl)

            lem₂ : (γ : coherent (iso f g H K))(x : X)
                 → to (from γ) x ≡ γ x
            lem₂ γ x =
              J (λ u v q → (z : f (g (f x)) ≡ f x)
                         → (r : v ≡ z)
                         → sym q ⊚ (q ⊚ r) ≡ r)
                (λ u z r → refl) _ _
                (left-unit (cong f (H x))) _
                (γ x)

    open _≅_ ≈⇔≅' public using ()
      renaming ( to to ≈⇒≅'
               ; from to ≅'⇒≈ )

    ≅⇒≈ : (X ≅ Y) → (X ≈ Y)
    ≅⇒≈ = ≅'⇒≈ ∘ ≅⇒≅'

open Properties public