{-# OPTIONS --without-K #-}

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Paths
open import lib.types.Unit
open import lib.types.Empty

module lib.Equivalences2 where

{- Pre- and post- composition with equivalences are equivalences -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         {h : A  B} (e : is-equiv h) where

  pre∘-is-equiv : is-equiv  (k : B  C)  k  h)
  pre∘-is-equiv = is-eq f g f-g g-f
    where f = λ k  k  h
          g = λ k  k  is-equiv.g e
          f-g = λ k  ap  q  λ x  k (q x)) (λ= $ is-equiv.g-f e)
          g-f = λ k  ap  q  λ x  k (q x)) (λ= $ is-equiv.f-g e)

  post∘-is-equiv : is-equiv  (k : C  A)  h  k)
  post∘-is-equiv = is-eq f g f-g g-f
    where f = λ k  h  k
          g = λ k  is-equiv.g e  k
          f-g = λ k  ap  q  q  k) (λ= $ is-equiv.f-g e)
          g-f = λ k  ap  q  q  k) (λ= $ is-equiv.g-f e)

{- The same thing on the abstraction level of equivalences -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         (e : A  B) where

  pre∘-equiv : (B  C)  (A  C)
  pre∘-equiv = (_ , pre∘-is-equiv (snd e))

  post∘-equiv : (C  A)  (C  B)
  post∘-equiv = (_ , post∘-is-equiv (snd e))


is-contr-map :  {i j} {A : Type i} {B : Type j} (f : A  B)
   Type (lmax i j)
is-contr-map {A = A} {B = B} f = (y : B)  is-contr (Σ A  x  f x == y))

equiv-is-contr-map :  {i j} {A : Type i} {B : Type j} {f : A  B}
   (is-equiv f  is-contr-map f)
equiv-is-contr-map e y =
   equiv-preserves-level ((equiv-Σ-fst  z  z == y) e) ⁻¹) (pathto-is-contr y)

contr-map-is-equiv :  {i j} {A : Type i} {B : Type j} {f : A  B}
   (is-contr-map f  is-equiv f)
contr-map-is-equiv {f = f} cm = is-eq _
   b  fst (fst (cm b)))
   b  snd (fst (cm b)))
   a  ap fst (snd (cm (f a)) (a , idp)))


fiber=-eqv :  {i j} {A : Type i} {B : Type j} {h : A  B} {y : B}
  (r s : Σ A  x  h x == y))
   (r == s)  Σ (fst r == fst s)  γ  ap h γ  snd s == snd r)
fiber=-eqv r s = equiv-Σ-snd  γ  !-equiv ∘e (↓-app=cst-eqv ⁻¹)) ∘e ((=Σ-eqv r s)⁻¹)


module _ {i j} {A : Type i} {B : Type j} where

  linv : (A  B)  Type (lmax i j)
  linv f = Σ (B  A)  g  (∀ x  g (f x) == x))

  rinv : (A  B)  Type (lmax i j)
  rinv f = Σ (B  A)  g  (∀ y  f (g y) == y))

  lcoh : (f : A  B)  linv f  Type (lmax i j)
  lcoh f (g , g-f) = Σ (∀ y  f (g y) == y)
                        f-g   y  ap g (f-g y) == g-f (g y))

  rcoh : (f : A  B)  rinv f  Type (lmax i j)
  rcoh f (g , f-g) = Σ (∀ x  g (f x) == x)
                        g-f   x  ap f (g-f x) == f-g (f x))


module _ {i j} {A : Type i} {B : Type j} {f : A  B} (e : is-equiv f) where

  equiv-linv-is-contr : is-contr (linv f)
  equiv-linv-is-contr = equiv-preserves-level (equiv-Σ-snd  _  λ=-equiv ⁻¹))
                          (equiv-is-contr-map (pre∘-is-equiv e) (idf A))

  equiv-rinv-is-contr : is-contr (rinv f)
  equiv-rinv-is-contr = equiv-preserves-level (equiv-Σ-snd  _  λ=-equiv ⁻¹))
                          (equiv-is-contr-map (post∘-is-equiv e) (idf B))

module _ {i j} {A : Type i} {B : Type j} {f : A  B} where

  rcoh-eqv : (v : rinv f)
     rcoh f v  Π A  x  (fst v (f x) , snd v (f x)) == (x , idp {a = f x}))
  rcoh-eqv v = equiv-Π-r  x  ((fiber=-eqv {h = f} _ _)⁻¹) ∘e apply-unit-r x) ∘e choice ⁻¹
    where
      apply-unit-r :  x  Σ _  γ  ap f γ == _)  Σ _  γ  ap f γ  idp == _)
      apply-unit-r x = equiv-Σ-snd $
        λ γ  coe-equiv (ap  q  q == snd v (f x)) (! (∙-unit-r _)))

  lcoh-eqv : (v : linv f)
     lcoh f v  Π B  y  (f (fst v y) , snd v (fst v y)) == (y , idp))
  lcoh-eqv v = equiv-Π-r  y  ((fiber=-eqv {h = fst v} _ _)⁻¹) ∘e apply-unit-r y) ∘e choice ⁻¹
    where
      apply-unit-r :  y  Σ _  γ  ap (fst v) γ == _)  Σ _  γ  ap (fst v) γ  idp == _)
      apply-unit-r y = equiv-Σ-snd $
        λ γ  coe-equiv (ap  q  q == snd v (fst v y)) (! (∙-unit-r _)))


equiv-rcoh-is-contr :  {i j} {A : Type i} {B : Type j} {f : A  B}
                      (e : is-equiv f)  (v : rinv f)  is-contr (rcoh f v)
equiv-rcoh-is-contr {f = f} e v = equiv-preserves-level ((rcoh-eqv v)⁻¹)
  (Π-level  x  =-preserves-level ⟨-2⟩ (equiv-is-contr-map e (f x))))

rinv-and-rcoh-eqv-is-equiv :  {i j} {A : Type i} {B : Type j} {h : A  B}
   Σ (rinv h) (rcoh h)  is-equiv h
rinv-and-rcoh-eqv-is-equiv {h = h} = equiv f g  _  idp)  _  idp)
  where f : Σ (rinv h) (rcoh h)  is-equiv h
        f s = record {g = fst (fst s); f-g = snd (fst s);
                      g-f = fst (snd s); adj = snd (snd s)}
        g : is-equiv h  Σ (rinv h) (rcoh h)
        g t = ((is-equiv.g t , is-equiv.f-g t) , (is-equiv.g-f t , is-equiv.adj t))

is-equiv-is-prop :  {i j} {A : Type i} {B : Type j} (f : A  B)
   is-prop (is-equiv f)
is-equiv-is-prop _ = inhab-to-contr-is-prop $ λ e 
  equiv-preserves-level rinv-and-rcoh-eqv-is-equiv
    (Σ-level (equiv-rinv-is-contr e) (equiv-rcoh-is-contr e))

∘e-unit-r :  {i} {A B : Type i} (e : A  B)  (e ∘e ide A) == e
∘e-unit-r e =
  pair= idp (prop-has-all-paths (is-equiv-is-prop (fst e)) _ _)

ua-∘e :  {i} {A B : Type i}
  (e₁ : A  B) {C : Type i} (e₂ : B  C)  ua (e₂ ∘e e₁) == ua e₁  ua e₂
ua-∘e =
  equiv-induction
     {A} {B} e₁   {C}   (e₂ : B  C)  ua (e₂ ∘e e₁) == ua e₁  ua e₂)
     A  λ e₂  ap ua (∘e-unit-r e₂)  ap  w  (w  ua e₂)) (! (ua-η idp)))

{- Type former equivalences involving Empty may require λ=. -}
module _ {j} {B : Empty  Type j} where
  Σ₁-Empty : Σ Empty B  Empty
  Σ₁-Empty = equiv (⊥-rec  fst) ⊥-rec ⊥-elim (⊥-rec  fst)

  Π₁-Empty : Π Empty B  Unit
  Π₁-Empty = equiv (cst tt) (cst ⊥-elim)  _  contr-has-all-paths Unit-is-contr _ _)  _  λ= ⊥-elim)

Σ₂-Empty :  {i} {A : Type i}  Σ A  _  Empty)  Empty
Σ₂-Empty = equiv (⊥-rec  snd) ⊥-rec ⊥-elim (⊥-rec  snd)