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

module Univalence-to-funext where

open import lib.Base
open import lib.Equivalence
open import lib.Function
open import lib.PathGroupoid
open import lib.PathFunctor
open import lib.NType

--============================================================================--
--                      Generic paths in Σ types

module _ {i j} {A : Type i} {B : A → Type j} where
  Σ-path-pair : (v w : Σ A B) → Type (lmax i j)
  Σ-path-pair v w = Σ (fst v == fst w)
                      (λ p → transport B p (snd v) == snd w)

  pair→Σ= : {v w : Σ A B} → Σ-path-pair v w → v == w
  pair→Σ= (idp , idp) = idp

  Σ=→pair : {v w : Σ A B} → v == w → Σ-path-pair v w
  Σ=→pair idp = (idp , idp)

  Σ=→pair→Σ= : {v w : Σ A B} (p : v == w) → pair→Σ= (Σ=→pair p) == p
  Σ=→pair→Σ= idp = idp

  pair→Σ=→pair : {v w : Σ A B} (z : Σ-path-pair v w) →
                 Σ=→pair (pair→Σ= z) == z
  pair→Σ=→pair (idp , idp) = idp

  Σ=≃pair : {v w : Σ A B} → (v == w) ≃ (Σ-path-pair v w)
  Σ=≃pair = equiv Σ=→pair pair→Σ= pair→Σ=→pair Σ=→pair→Σ=

               
--============================================================================--
--                           Univalence

idtoeqv : ∀ {i} {A B : Type i} → (A == B) → (A ≃ B)
idtoeqv {A = A} idp = ide A

postulate
  ua : ∀ {i} {A B : Type i} → (A ≃ B) → (A == B)
  idtoeqv-ua-β : ∀ {i} {A B : Type i} (e : A ≃ B) → idtoeqv (ua e) == e

eqv-post∘ : ∀ {i} {A B : Type i} {C : Type i} (p : A == B) → 
            fst (idtoeqv (ap (λ T → (C → T)) p)) == _∘_ (fst (idtoeqv p))
eqv-post∘ idp = idp

--============================================================================--
--                         Happly and lemmas

module _ {i j} {A : Type i} {B : A → Type j} {f g : Π A B} where
  idh : f ∼ f
  idh a = idp

  happly : f == g → f ∼ g
  happly p a = ap (λ k → k a) p

  tr-happly-lemma : (p : f == g) →
                    transport (λ k → f ∼ k) p (idh) == happly p
  tr-happly-lemma idp = idp

  fib-happly-lemma : (h : f ∼ g) → ((f , idh) == (g , h)) ≃ hfiber happly h
  fib-happly-lemma h = (equiv from to α β) ∘e Σ=≃pair
    where
      to : hfiber happly h → Σ-path-pair (f , idh) (g , h)
      to (p , q) = (p , tr-happly-lemma p ∙ q)

      from :  Σ-path-pair (f , idh) (g , h) → hfiber happly h
      from (p , q) = (p , ! (tr-happly-lemma p) ∙ q)

      β : (b : Σ-path-pair (f , idh) (g , h)) → to (from b) == b
      β (p , q) = pair→Σ= (idp , ! (∙-assoc (tr-happly-lemma p)
                                            (! (tr-happly-lemma p)) q) ∙
                                 !-inv-r (tr-happly-lemma p) ∙2 idp)

      α : (a : hfiber happly h) → from (to a) == a
      α (p , q) = pair→Σ= (idp ,
                           ! (∙-assoc (! (tr-happly-lemma p))
                             (tr-happly-lemma p) q) ∙
                           !-inv-l (tr-happly-lemma p) ∙2 idp)

--============================================================================--
--                     Equivalences and contractibility

contr-retract : ∀ {i} {A B : Type i}
                (r : A → B) (s : B → A) →
                (r ∘ s ∼ (idf B)) →
                is-contr A → is-contr B
contr-retract r s h p = has-level-in
                      ((r (fst c)) , λ y → ap r (snd c (s y)) ∙ h y)
                      where c = has-level-apply p
                      
module _ {i j} {A : Type i} {B : Type j} where
  is-contr-map : (f : A → B) → Type (lmax i j)
  is-contr-map f = (y : B) → is-contr (hfiber f y)

  tr-ap-lemma : (f : A → B) {a' a : A} {b : B}
                (p : a' == a) (q : f a' == b) →
                transport (λ x → f x == b) p q == ! (ap f p) ∙ q
  tr-ap-lemma f idp idp = idp

  nat-lemma : {k l : B → B} {a b : B} (p : a == b )(h : k ∼ l) →
              ap k p ∙ h b == h a ∙ ap l p
  nat-lemma {a = a} idp h = ! (∙-unit-r (h a))

  contr-map-is-equiv : {f : A → B} → (is-contr-map f → is-equiv f)
  contr-map-is-equiv {f = f} c = snd (equiv f g α β)
    where
      g : B → A
      g b = fst (fst (has-level-apply (c b)))

      α : f ∘ g ∼ (idf B)
      α b = snd (fst (has-level-apply (c b)))

      β : g ∘ f ∼ (idf A)
      β a = fst (Σ=→pair (snd (has-level-apply (c (f a))) (a , idp)))

      

  equiv-is-contr-map : {f : A → B} → (is-equiv f → is-contr-map f)
  equiv-is-contr-map {f = f} e b =
                        has-level-in (hf , λ y → pair→Σ= (fc y , sc y))
    where
      g : B → A
      g = is-equiv.g e

      α : g ∘ f ∼ (idf A)
      α = is-equiv.g-f e

      β : f ∘ g ∼ (idf B)
      β = is-equiv.f-g e
      
      hf : hfiber f b
      hf = ((g b) , (β b))

      fc : (y : hfiber f b) → (g b) == fst y
      fc (a , p) = ap (g) (! p) ∙ α a

      sc : (y : hfiber f b) →
           transport (λ x → f x == b) (fc (fst y , snd y)) (β b) == snd y
      sc (a , p) =
        transport (λ x → f x == b) (fc (a , p)) (β b)
          =⟨ tr-ap-lemma f (fc (a , p)) (β b) ⟩
        ! (ap f  (fc (a , p))) ∙ (β b)
          =⟨ ap ! (ap-∙ f (ap g (! p)) (α a)) ∙2 idp ⟩
        ! (ap f (ap g (! p)) ∙ ap f (α a)) ∙ (β b)
          =⟨ ap ! (idp ∙2 is-equiv.adj e a) ∙2 idp {a = β b}⟩
        ! (ap f (ap g (! p)) ∙ (β (f a))) ∙ (β b)
          =⟨ ap ! (∘-ap f g (! p) ∙2 idp) ∙2 idp ⟩
        ! (ap (f ∘ g) (! p) ∙ (β (f a))) ∙ (β b)
          =⟨ !-∙ (ap (f ∘ g) (! p)) (β (f a)) ∙2 idp ⟩
        (! (β (f a)) ∙ ! (ap (λ x → f (g x)) (! p))) ∙ (β b)
          =⟨ (idp ∙2 !-ap (f ∘ g) (! p)) ∙2 idp {a = β b}⟩
        (! (β (f a)) ∙ (ap (f ∘ g) (! (! p)))) ∙ (β b)
          =⟨ (idp ∙2 ap (ap (f ∘ g)) (!-! p)) ∙2 idp {a = β b} ⟩
        (! (β (f a)) ∙ (ap (f ∘ g) p)) ∙ (β b)
          =⟨ ∙-assoc (! (β (f a))) (ap (f ∘ g) p) (β b) ⟩
        ! (β (f a)) ∙ (ap (f ∘ g) p ∙ (β b))
          =⟨ idp {a = ! (β (f a))} ∙2 (nat-lemma p β ∙ (idp ∙2 ap-idf p)) ⟩
        ! (β (f a)) ∙ (β (f a) ∙ p)
          =⟨ ! (∙-assoc (! (β (f a))) (β (f a)) p) ⟩
        (! (β (f a)) ∙ β (f a)) ∙ p
          =⟨ !-inv-l (β (f a)) ∙2 idp ⟩
        p
          =∎

      

--============================================================================--
--                        Univalence implies funext

module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where
  image : A → Type i
  image a = Σ (B a) (λ b → f a == b)

  graphType : Type i
  graphType = Σ A image
  
  prA : graphType → A
  prA = fst

  prA-is-equiv : graphType ≃ A
  prA-is-equiv = equiv prA (λ x → (x , f x , idp)) (λ b → idp) β
    where
      tr-post-concat : ∀ {i} {X : Type i} {x y z : X} {p : x == y}
                 (q : z == x) → transport (_==_ z) p q == q ∙ p
      tr-post-concat {p = idp} idp = idp

      β : (a : graphType) → (fst a , f (fst a), idp) == a
      β (a , b , p) = pair→Σ= (idp , (pair→Σ= (p , (tr-post-concat idp))))
                
  fibreOverId : Type i
  fibreOverId = hfiber (_∘_ prA) (idf A)

  fibreOverId-is-contr : is-contr fibreOverId
  fibreOverId-is-contr = prA∘-is-equiv (idf A)
       where
        p : graphType == A
        p = ua prA-is-equiv

        pβ : fst (idtoeqv p) == prA
        pβ = ap fst (idtoeqv-ua-β prA-is-equiv)
        
        prA∘-is-equiv : is-contr-map (λ g → prA ∘ g)
        prA∘-is-equiv = transport is-contr-map
                         (eqv-post∘ p ∙ ap (λ x → _∘_ x) pβ)
                         (equiv-is-contr-map
                           (snd (idtoeqv (ap (λ T → (A → T)) p))))

  homotopyType : Type i
  homotopyType = Σ (Π A B) (λ g → f ∼ g)

  -- We crucially make use of the η-rule for functions here
  s : homotopyType → fibreOverId
  s (g , h) = ((λ a → (a , g a , h a)) , idp)

  r : fibreOverId → homotopyType
  r (func , p) = fst ∘ img , snd ∘ img
               where
                 img : (a : A) → image a
                 img a = transport image (happly p a) (snd (func a))

  -- and here
  var-funext : is-prop homotopyType
  var-funext = contr-is-prop (contr-retract r s (λ _ → idp)
                              fibreOverId-is-contr)

module _ {i} {A : Type i} {B : A → Type i} {f g : Π A B} where
  pre-funext : (h : f ∼ g) → is-contr ((f , idh {g = g}) == (g , h))
  pre-funext h = has-level-apply var-funext (f , idh {g = g}) (g , h)

  funext : is-equiv (happly {f = f}{g = g})
  funext = contr-map-is-equiv
             λ h → equiv-preserves-level
                     (fib-happly-lemma h)
                     ⦃ pre-funext h ⦄