{-# OPTIONS --rewriting #-}

open import Agda.Primitive using (lzero; Level; _⊔_)

open import Lib
open import Kan
open import Interval
open import Cofibs
open import Path
open import Contractible

module Equiv where

  -- normal definition

  isEquiv : {l1 l2 : Level} (A : Set l1) (B : Set l2) (f : A → B) → Set (l1 ⊔ l2)
  isEquiv A B f = (b : B) → Contractible (HFiber f b)

  Equiv : {l1 l2 : Level} (A : Set l1) (B : Set l2) → Set (l1 ⊔ l2)
  Equiv A B = Σ \ (f : A → B) → isEquiv A B f

  id-Equiv : ∀ {l} {A : Set l} → hasHCom A → isEquiv A A (\ x → x)
  id-Equiv hcomA = λ a → (a , (\ _ → a) , id , id) , (s a) where
    abstract
      s = \ a → (\ hf → snd (scontr hcomA a) hf )

  QEquiv : {l1 l2 : Level} (A : Set l1) (B : Set l2) → Set (l1 ⊔ l2)
  QEquiv A B = Σ \ (f : A → B) → Σ \ (g : B → A) → ((x : A) → Path A ((g o f) x) x) × ((y : B) → Path B ((f o g) y) y)

  Equiv-to-QEquiv : {l1 l2 : Level} (A : Set l1) (B : Set l2) → Equiv A B → QEquiv A B
  Equiv-to-QEquiv A B (f , eq) = f , g , eq1 , eq2 where
  
    g : B → A
    g b = fst (fst (eq b))

    h1 : (a : A) → _
    h1 a = snd (eq (f a)) (a , eq-to-Path _ _ id)

    eq1 : (a : A) → _
    eq1 a =  (λ i → fst (fst (h1 a) i))
             , ap fst (fst (snd (h1 a)))
             , ap fst (snd (snd (h1 a)))

    eq2 : (b : B) → _
    eq2 b = snd (fst (eq b))

  -- ----------------------------------------------------------------------
  -- other definitions of equivalence

  -- filling instead of normal def of contractibility

  isEquivFill : {l1 l2 : Level} (A : Set l1) (B : Set l2) (f : A → B) → Set (ℓ₁ ⊔ l1 ⊔ l2)
  isEquivFill A B f = (b : B) → ContractibleFill (HFiber f b)

  isEquiv-isEquivFill : {l1 l2 : Level} (A : Set l1) (B : Set l2) (f : A → B) → isEquiv A B f → ((b : B) → hasHCom (HFiber f b)) → isEquivFill A B f
  isEquiv-isEquivFill A B f e hcomHFB b = contr-extend-partial (hcomHFB b) (e b)

  EquivFill : {l1 l2 : Level} (A : Set l1) (B : Set l2) → Set _
  EquivFill A B = Σ \ (f : A → B) → isEquivFill A B f

  transport-IsEquivFill : ∀ {l1 l2 : Level} {A A' : Set l1} {B : Set l2}
                            {f : A' → B} → isEquivFill A' B f
                            → (p : A == A')
                            → isEquivFill A B (f o coe p)
  transport-IsEquivFill e id = e

  -- ----------------------------------------------------------------------

  isEquivFill-hprop : {l1 l2 : Level} → (A : Set l1) (B : Set l2) (f : A → B) 
                → (e1 e2 : isEquivFill A B f)
                → Path (isEquivFill A B f) e1 e2
  isEquivFill-hprop A B f e1 e2 = (\ z → \ b → fst (ContractibleFill-hprop _ (e1 b) (e2 b)) z) ,
                                  (λ= \ b → fst (snd (ContractibleFill-hprop (HFiber f b) (e1 b) (e2 b)))) ,
                                  (λ= \ b → snd (snd (ContractibleFill-hprop (HFiber f b) (e1 b) (e2 b))))

  hcomΠ : ∀ {l1 l2 : Level} (A : Set l1) (B : A → Set l2)
           → ((x : A) → hasHCom (B x) )
           → hasHCom ( (x : A) → B x)
  hcomΠ A B comB r r' α t b = (λ a → fst (fillb a)) , (λ pα → λ= λ a → fst (snd (fillb a)) pα) , (λ {id → λ= (λ a → snd (snd (fillb a)) id)}) where
  
    fillb : ∀ a → _
    fillb a = comB a r r' α (λ z pα → (t z pα) a) ((fst b) a , (λ pα → ap (λ f → f a) (snd b pα)))
    
  fix-isEquiv : {l1 l2 : Level} (A : Set l1) (B : Set l2) (f : A → B) 
              → (isEquivFill A B f)
              → ContractibleFill (isEquivFill A B f)
  fix-isEquiv A B f b = inhabited-hprop-contractible _ (hcomΠ _ _ (\ x → hcomContractibleFill _)) b (isEquivFill-hprop A B f)

  abstract
    idEquiv-from-= : ∀ {l}{A B : Set l}(comA : hasHCom A)(f : A → B)(eq : A == B) → f == coe (ap (λ X → (A → X)) eq) (λ x → x) → isEquiv A B f
    idEquiv-from-= comA f id id a = scontr comA a