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

open import level using (lsuc; _⊔_)
open import equality.core

Extensionality :  i j  Set (lsuc (i  j))
Extensionality i j = {X : Set i}{Y : Set j}
                    {f g : X  Y}
                    ((x : X)  f x  g x)
                    f  g

Extensionality' :  i j  Set (lsuc (i  j))
Extensionality' i j = {X : Set i}{Y : X  Set j}
                     {f g : (x : X)  Y x}
                     ((x : X)  f x  g x)
                     f  g

StrongExt :  i j  Set (lsuc (i  j))
StrongExt i j = {X : Set i}{Y : X  Set j}
               {f g : (x : X)  Y x}
               (∀ x  f x  g x)  (f  g)

funext-inv :  {i j}{X : Set i}{Y : X  Set j}
         {f g : (x : X)  Y x}
         f  g
         (x : X)  f x  g x
funext-inv refl x = refl