Removed the postulate about funext

Univalence.agda

{-# OPTIONS --cubical --rewriting #-}

module cubical.Univalence where

open import Cubical.Core.Everything
  using (_∧_; _∨_;  ~_; i0;i1 ; transp; Σ; fst; snd
        ; Glue ; glue ; unglue ; lineToEquiv)
  renaming (_≃_ to _≃c_; _,_ to _,c_)

open import Cubical.Foundations.Prelude
  using (transportRefl; _≡⟨_⟩_; _∎)
  renaming ( _≡_           to _≡c_
           ; refl          to refl-c
           ; transport     to transport-c
           ; J             to J-c
           ; JRefl         to J-cRefl
           ; sym           to !-c
           ; _∙_           to ·-c
           ; cong          to cong-c
           ; isContr       to isContr-c
           ; isProp        to isProp-c
           ; isSet         to isSet-c
           ; funExt        to funext-c
           ; funExt⁻       to happly-c
           ; subst         to subst-c
           ; isPropIsContr to isPropIsContr-c
           )

open import Cubical.Foundations.Equiv
  using ( idEquiv; equivToIso; compEquiv; isPropIsEquiv
        ; equivEq ; invEq ; retEq ; secEq ; funIsEq )
  renaming ( isEquiv to isEquiv-c
           ; fiber   to fiber-c)
open import Cubical.Foundations.Isomorphism
  using ( isoToEquiv; iso; Iso)

open import Cubical.Foundations.Univalence
    renaming ( ua              to ua-c
             ; pathToEquiv     to idtoeqv-c
             ; pathToEquiv-ua  to ua-β-c
             ; ua-pathToEquiv  to ua-η-c
             ; univalence      to eqvUnivalence-c
             ; univalenceIso   to univalenceIso-c )

open import foundations.BasicTypes
  using ( refl; Level; Type; idp; Eq; proj₁; proj₂ ; _,_)
open import foundations.BasicFunctions using ( ap )
open import foundations.EquivalenceType
  using (_≃_;isEquiv; lrmap-inverse ; rlmap-inverse)
open import foundations.FibreType   using ( fiber )
open import foundations.HLevelTypes using (isContr)

variable
  ℓ  : Level
  A : Type ℓ

{- The following actually appears in Cubical.Data.Equality -}

module _ {x y : A} where
  eqToPath : Eq x y → x ≡c y
  eqToPath idp i = x

  pathToEq : x ≡c y → Eq x y
  pathToEq p = transp (λ i → Eq x (p i)) i0 (refl x)

module _ {x y : A} where
  eqToPath-pathToEq : (p : x ≡c y) → (eqToPath (pathToEq p)) ≡c p
  eqToPath-pathToEq p
    = J-c (λ _ h → eqToPath (pathToEq h) ≡c h) (cong-c eqToPath (transportRefl (refl x))) p

  pathToEq-eqToPath : (p : Eq x y) → pathToEq (eqToPath p) ≡c p
  pathToEq-eqToPath idp = transportRefl idp

Eq≃Path : ∀ {ℓ}{A : Type ℓ} {x y : A} → (Eq x y) ≃c (x ≡c y)
Eq≃Path = isoToEquiv (iso eqToPath pathToEq eqToPath-pathToEq pathToEq-eqToPath)

Path≡Eq : ∀ {ℓ} {A : Set ℓ} → {x y : A}
  → (Eq x y) ≡c (x ≡c y)
Path≡Eq = ua-c Eq≃Path

path-to-≃c : {A B : Type ℓ} → A ≡c B → A ≃c B
path-to-≃c p = lineToEquiv (λ i → p i)

isContr≡isContr-c : ∀ {ℓ} {A : Set ℓ} → (isContr A) ≡c (isContr-c A)
isContr≡isContr-c {A = A} i = Σ A (λ x → (y : A) → Path≡Eq {x = x} {y} i)

module _ {ℓ₁ ℓ₂} {A : Set ℓ₁}{B : Set ℓ₂} (f : A → B) where

  fiber≡fiber-c  : (b : B) → (fiber f b) ≡c (fiber-c f b)
  fiber≡fiber-c b i = Σ A λ (x : A) → Path≡Eq {x = f x} {b} i

  isEquiv≡isEquiv-c' : isEquiv f ≡c ((b : B) → isContr-c (fiber-c f b))
  isEquiv≡isEquiv-c' = λ i → (b : B) → isContr≡isContr-c {A = fiber≡fiber-c b i} i

  isEquiv≃cisEquiv-c : ((b : B) → isContr-c (fiber-c f b)) ≃c (isEquiv-c f)
  isEquiv≃cisEquiv-c = isoToEquiv (iso go back  go-back back-go )
    where
    go : ((b : B) → isContr-c (fiber-c f b)) → (isEquiv-c f)
    isEquiv-c.equiv-proof (go f-is-equiv) = f-is-equiv

    back : (isEquiv-c f) → ((b : B) → isContr-c (fiber-c f b))
    back r = isEquiv-c.equiv-proof r

    go-back : (p : (isEquiv-c f)) → go (back p) ≡c p
    go-back p = isPropIsEquiv f _ _

    back-go : (p : _) → back (go p) ≡c p
    back-go q = funext-c λ b → isPropIsContr-c _ _

  isEquiv≡cisEquiv-c : isEquiv f ≡c isEquiv-c f
  isEquiv≡cisEquiv-c = ·-c isEquiv≡isEquiv-c' (ua-c isEquiv≃cisEquiv-c)

  equiv-≡ : (f , isEquiv f) ≡c (f , isEquiv-c f)
  equiv-≡ = λ i → (f , isEquiv≡cisEquiv-c i)

module _ {ℓ₁ ℓ₂} {A : Set ℓ₁}{B : Set ℓ₂} where
  ≃-≡-≃c : (A ≃ B) ≡c (A ≃c B)
  ≃-≡-≃c = λ i → Σ (A → B) (λ f → isEquiv≡cisEquiv-c f i)

  ≃-≃c-≃c : (A ≃ B) ≃c (A ≃c B)
  ≃-≃c-≃c = idtoeqv-c ≃-≡-≃c

  ≃-to-≃c : A ≃ B → A ≃c B
  ≃-to-≃c  = fst  ≃-≃c-≃c

  ≃c-to-≃ : A ≃c B → A ≃ B
  ≃c-to-≃  = invEq ≃-≃c-≃c

module _  {ℓ₁ ℓ₂ : Level}{A : Type ℓ₁} {B : A → Type ℓ₂}
  {f g : (a : A) → B a} where
  funext
    : ((x : A) → Eq (f x) (g x))
    ----------------------------
    → Eq f g
  funext p = pathToEq (λ i x → eqToPath (p x) i)

  happly
    : Eq f g
    ------------------------
    → ((x : A) → Eq (f x) (g x))
  happly p a = pathToEq λ i → (eqToPath p) i a
  ≡-app = happly

  eqFunExt' : (Eq f g) ≃c ((x : A) → Eq (f x) (g x))
  eqFunExt' = isoToEquiv (iso happly funext go back)
    where
    go : (b : (x : A) → Eq (f x) (g x) ) 
      → happly (funext b) ≡c b
    go b = happly (funext b) 
         ≡⟨ funext-c (λ a → cong-c (λ o → pathToEq (λ i → (o i a))) 
                    (eqToPath-pathToEq {x = f}{y = g} (λ j x → eqToPath (b x) j))) ⟩  
         (λ a → pathToEq (eqToPath (b a)))
         ≡⟨ funext-c (λ a → pathToEq-eqToPath (b a)) ⟩ 
         b ∎

    back : (b : Eq f g) → funext (happly b) ≡c b
    back b = funext (happly b)
      ≡⟨ refl-c ⟩ 
      pathToEq (λ i x → eqToPath (((happly b)) x) i)
      ≡⟨ refl-c ⟩ 
       pathToEq (λ i x → eqToPath ((pathToEq (λ j → (eqToPath b) j x))) i)
      ≡⟨ cong-c pathToEq
          (λ k → funext-c (λ x → eqToPath-pathToEq {x = f x}{y = g x} 
                          (λ j → (eqToPath b) j x) k)) ⟩ 
      pathToEq (λ i x → (eqToPath b) i x)
        ≡⟨ cong-c pathToEq refl-c ⟩ 
      pathToEq (eqToPath b)
        ≡⟨ pathToEq-eqToPath b ⟩ 
      b ∎

module  _ {ℓ} {A B : Set ℓ} where
  ua : A ≃ B → Eq A B
  ua e = pathToEq (ua-c (≃-to-≃c e))

  idtoeqv : Eq A B → A ≃ B
  idtoeqv e = ≃c-to-≃ (idtoeqv-c (eqToPath e))

  ua-η'
    : (e : Eq A B)
    ---------------------
    → (ua (idtoeqv e)) ≡c e

  ua-η' e =
    (ua (idtoeqv e))
      ≡⟨ refl-c ⟩
    pathToEq (ua-c (≃-to-≃c (≃c-to-≃ (idtoeqv-c (eqToPath e)))))
      ≡⟨ cong-c (λ o → pathToEq (ua-c o)) (retEq ≃-≃c-≃c (idtoeqv-c (eqToPath e))) ⟩
    pathToEq (ua-c  (idtoeqv-c (eqToPath e)))
      ≡⟨ cong-c (λ o → pathToEq o) (ua-η-c (eqToPath e)) ⟩
    pathToEq (eqToPath e)
      ≡⟨ secEq Eq≃Path e ⟩
    e ∎

  ua-β'
    : (e : A ≃ B)
    ----------------------
    → (idtoeqv (ua e)) ≡c e

  ua-β' e =
    (idtoeqv (ua e))
      ≡⟨ refl-c ⟩
    ≃c-to-≃ (idtoeqv-c (eqToPath (pathToEq (ua-c (≃-to-≃c e)))))
      ≡⟨ cong-c (λ o → ≃c-to-≃ (idtoeqv-c o)) (retEq Eq≃Path (ua-c (≃-to-≃c e))) ⟩
    ≃c-to-≃ (idtoeqv-c (ua-c (≃-to-≃c e)))
      ≡⟨ cong-c (λ o → ≃c-to-≃ o) (ua-β-c (≃-to-≃c e)) ⟩
    ≃c-to-≃ (≃-to-≃c e)
      ≡⟨ secEq ≃-≃c-≃c e ⟩
    e ∎

  eqvUnivalence' : (Eq A B) ≃c (A ≃ B)
  eqvUnivalence' = isoToEquiv (iso idtoeqv ua ua-β' ua-η')

  eqvUnivalence : (Eq A B) ≃ (A ≃ B)
  eqvUnivalence  = ≃c-to-≃ eqvUnivalence'

  ua-η : (e : Eq A B) → Eq (ua (idtoeqv e)) e
  ua-η e = pathToEq (ua-η' e)

  ua-β : (e : A ≃ B) → Eq (idtoeqv (ua e)) e
  ua-β e = pathToEq (ua-β' e)