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

open import level using (_⊔_; ↑; lift)
open import sets.unit
open import sum
open import equality.core
open import equality.calculus
open import function.core using (_∘_; const)
open import function.extensionality.core
open import function.extensionality.nondep

open import hott.hlevel.core
open import hott.hlevel.properties

abstract
  ext₀' : ∀ {i j} → Extensionality' i j
  ext₀' {i} {j} {X = X} {Y = Y} {f}{g} h = cong (λ u → proj₁ ∘ u) p
    where
      U : (x : X) → Set j
      U x = singleton (f x)

      U-contr : contr ((x : X) → U x)
      U-contr = Π-contr (λ x → singl-contr (f x))

      f* : (x : X) → U x
      f* x = f x , refl

      g* : (x : X) → U x
      g* x = g x , h x

      p : f* ≡ g*
      p = contr⇒prop U-contr f* g*

abstract
  ext' : ∀ {i j} → Extensionality' i j
  ext' h = ext₀' h ⊚ ext₀' (λ _ → refl) ⁻¹

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