{-# 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))