{-# OPTIONS --rewriting #-}

module Equivalence where

open import Contractible
open import Equality
open import EquationalReasoning
open import Fibration
open import Function
open import Interval
open import Level
open import Path
open import Product
open import Sigma

----------------------------------------------------------------------
-- Homotopy fibres
----------------------------------------------------------------------
~fibre :
  {ℓ : Level}
  {A B : Set ℓ}
  (f : A → B)
  (y : B)
  → -----------
  Set ℓ
~fibre {A = A} f y = Σ x ∈ A , f x ~ y

----------------------------------------------------------------------
-- Equivalence
----------------------------------------------------------------------
record isEquiv {ℓ : Level}{A B : Set ℓ}(f : A → B) : Set ℓ where
  field
    instance {{iscontr}} : (y : B) → isContr (~fibre f y)

open isEquiv{{...}} public

----------------------------------------------------------------------
-- Quasi-inverses
----------------------------------------------------------------------
record qInv  {ℓ : Level}{A B : Set ℓ}(f : A → B) : Set ℓ where
  constructor mkqinv
  field
    inv  : B → A
    invl : (x : A) → x ~ inv (f x)
    invr : (y : B) → y ~ f (inv y)

open qInv {{...}} public

-- qInv2Equiv :
--   {ℓ : Level}
--   {A B : Set ℓ}
--   (f : A → B)
--   → ----------------
--   qInv f → isEquiv f
-- centre  {{iscontr {{qInv2Equiv f (mkqinv g α β)}} y}}         =
--   (g y , ~symm (β y))
-- ~centre {{iscontr {{qInv2Equiv f (mkqinv g α β)}} y}} (x , p) =
--   {!!}

----------------------------------------------------------------------
-- Path of fibrations
----------------------------------------------------------------------
∂ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  → -------------------------
  𝕀 → Fib ℓ (Γ × 𝕀) → Fib ℓ Γ
∂ i = Fib' (_, i)

infix  _≈_
data
  _≈_
    {ℓ ℓ' : Level}
    {Γ : Set ℓ'}
    : ---------------------------------
    (A B : Fib ℓ Γ) → Set (lsuc ℓ ⊔ ℓ')
  where
  ≈path : (Φ : Fib ℓ (Γ × 𝕀)) → ∂ O Φ ≈ ∂ I Φ

infixl  _At_
_At_ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  {A B : Fib ℓ Γ}
  (Φ : A ≈ B)
  → -------------
  𝕀 → Fib ℓ Γ
(≈path Φ) At i = ∂ i Φ

AtO :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  {A B : Fib ℓ Γ}
  (P : A ≈ B)
  → -------------
  P At O ≡ A
AtO (≈path _) = refl

AtI :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  {A B : Fib ℓ Γ}
  (P : A ≈ B)
  → -------------
  P At I ≡ B
AtI (≈path _) = refl

{-# REWRITE AtO AtI #-}

----------------------------------------------------------------------
-- Degenerate path of fibrations
----------------------------------------------------------------------
≈Refl :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  (A : Fib ℓ Γ)
  → ------------
  A ≈ A
≈Refl A  = ≈path (Fib' fst A)

----------------------------------------------------------------------
-- Composing paths of fibrations
----------------------------------------------------------------------
_⊙_ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  {A B C : Γ → Set ℓ}
  (Q : (x : Γ) → B x ~ C x)
  (P : (x : Γ) → A x ~ B x)
  → -----------------------
  (x : Γ) → A x ~ C x
(Q ⊙ P) x = Q x ∙ P x

  
-- ≈comp :
--   {ℓ ℓ' : Level}
--   {Γ : Set ℓ'}
--   (Φ Ψ : Fib ℓ (Γ × 𝕀))
--   (u : ∂ I Φ ≡ ∂ O Ψ)
--   → -------------------
--   Fib ℓ (Γ × 𝕀)
-- fst (≈comp (F , _) (G , _) u) (x , i) =
--   (~comp (F ∘ (x ,_)) (G ∘ (x ,_)) (cong (λ Θ → (fst Θ) x) u )) i
-- fst (snd (≈comp (F , φ₁ , φ₂) (G , ψ₁ , ψ₂) u)) .(f O) .(f I) (path f) a = {!!}
-- snd (snd (≈comp Φ Ψ u)) = {!!}
  
-- infixr 5 _⊙_
-- _⊙_ :
--   {ℓ ℓ' : Level}
--   {Γ : Set ℓ'}
--   {A B C : Fib ℓ Γ}
--   → -------------------
--   B ≈ C → A ≈ B → A ≈ C
-- Q ⊙ P  = {!!}

----------------------------------------------------------------------
-- Converting paths of fibrations to equivalences
----------------------------------------------------------------------
≈coe :
  {Γ : Set}
  {A B : Γ → Set}
  {α : isFib A}
  {β : isFib B}
  (P : (A , α) ≈ (B , β))
  → ---------------------
  (x : Γ) → A x → B x
≈coe (≈path (_ , φ)) x = ~subst φ (~cong (x ,_) (O to I))

qInv≈coe :
  {Γ : Set}
  {A B : Γ → Set}
  {α : isFib A}
  {β : isFib B}
  (P : (A , α) ≈ (B , β))
  (x : Γ)
  → ---------------------
  qInv (≈coe P x)
inv  {{qInv≈coe (≈path (F , φ)) x}}    =
  ~subst φ (~cong (x ,_) (I to O))
invl {{qInv≈coe (≈path (F , φ)) x}} a₀ =
  let
    γ = (x ,_)
    p = ~cong γ (O to I)
    q = ~cong γ (I to O)
  in
  path:
    a₀
  ~[ ~substrefl φ a₀ ]
    ~subst φ (~cong γ (~refl O)) a₀
  ~[ ~cong (λ r → ~subst φ (~cong γ r) a₀)
     (~𝕀uniq (~refl O) (I to O ∙ O to I)) ]
    ~subst φ (~cong γ (I to O ∙ O to I)) a₀
  ~[ ≡to~ (cong (λ r → ~subst φ r a₀) (~cong∙ γ (I to O) (O to I))) ]
    ~subst φ (q ∙ p) a₀
  ~[ ~substassoc {{φ}} q p a₀ ]
    ~subst φ q (~subst φ p a₀)
  endp
invr {{qInv≈coe (≈path (F , φ)) x}} a₁ = let
    γ = (x ,_)
    p = ~cong γ (O to I)
    q = ~cong γ (I to O)
  in
  path:
    a₁
  ~[ ~substrefl φ a₁ ]
    ~subst φ (~refl (x , I)) a₁
  ~[ ~cong (λ r → ~subst φ (~cong γ r) a₁)
     (~𝕀uniq (~refl I) (O to I ∙ I to O)) ] 
    ~subst φ (~cong γ (O to I ∙ I to O)) a₁
  ~[ ≡to~ (cong (λ r → ~subst φ r a₁) (~cong∙ γ (O to I) (I to O))) ]
    ~subst φ (p ∙ q) a₁
  ~[ ~substassoc {{φ}} p q a₁ ]
    ~subst φ p (~subst φ q a₁)
  endp