{-# OPTIONS --without-K #-}
module function.extensionality.proof where

open import level
open import sum
open import equality
open import function.extensionality.core
open import hott.univalence
open import hott.level.core
open import hott.level.closure.core
open import hott.level.sets.core
open import hott.equivalence.core
open import sets.unit

-- this uses definitional η for ⊤
contr-exp-⊤ : ∀ {i j}{A : Set i} → contr (A → ⊤ {j})
contr-exp-⊤ = (λ _ → tt) , (λ f → refl)

module Weak where
  →-contr : ∀ {i j}{A : Set i}{B : Set j}
          → contr B
          → contr (A → B)
  →-contr {A = A}{B = B} hB = subst contr p contr-exp-⊤
    where
      p : (A → ⊤) ≡ (A → B)
      p = ap (λ X → A → X) (unique-contr ⊤-contr hB)

  funext : ∀ {i j}{A : Set i}{B : Set j}
      → (f : A → B)(b : B)(h : (x : A) → b ≡ f x)
      → (λ _ → b) ≡ f
  funext f b h =
    ap (λ u x → proj₁ (u x))
         (contr⇒prop (→-contr (singl-contr b))
                      (λ _ → (b , refl))
                      (λ x → f x , h x))

abstract
  Π-contr : ∀ {i j}{A : Set i}{B : A → Set j}
          → ((x : A) → contr (B x))
          → contr ((x : A) → B x)
  Π-contr {i}{j}{A}{B} hB = subst contr p contr-exp-⊤
    where
      p₀ : (λ _ → ⊤) ≡ B
      p₀ = Weak.funext B ⊤ (λ x → unique-contr ⊤-contr (hB x))

      p : (A → ⊤ {j}) ≡ ((x : A) → B x)
      p = ap (λ Z → (x : A) → Z x) p₀

  private
    funext₀ : ∀ {i j} → Extensionality' i j
    funext₀ {i}{j}{X = X}{Y = Y}{f = f}{g = g} h = ap (λ u x → proj₁ (u x)) lem
      where
        C : X → Set j
        C x = Σ (Y x) λ y → f x ≡ y

        f' g' : (x : X) → C x
        f' x = (f x , refl)
        g' x = (g x , h x)

        lem : f' ≡ g'
        lem = contr⇒prop (Π-contr (λ x → singl-contr (f x))) f' g'

abstract
  funext : ∀ {i j} → Extensionality' i j
  funext h = funext₀ h · sym (funext₀ (λ _ → refl))

  funext-id : ∀ {i j}{X : Set i}{Y : X → Set j}
         → (f : (x : X) → Y x)
         → funext (λ x → refl {x = f x}) ≡ refl
  funext-id _ = left-inverse (funext₀ (λ _ → refl))