{-# OPTIONS --type-in-type #-}

open import NeilPrelude

module Extensionality where

Extensionality : Set
Extensionality = ({A : Set}  {B : SetΠ A}  {f g : Π A B}  ((a : A)  f a  g a)  f  g)
               ×
                 ({A : Set}  {B : SetΠ A}  {f g : {a : A}  B a}  ({a : A}  f {a}  g {a})  _≡_ {_} { {a : A}  B a } f g)

ext : {{ex : Extensionality}}  {A : Set}  {B : SetΠ A}  {f g : Π A B}  ((a : A)  f a  g a)  f  g
ext {{ex}} = fst ex

ext' : {{ex : Extensionality}}  {A : Set}  {B : SetΠ A}  {f g : Π A B}  ({a : A}  f a  g a)  f  g
ext' = ext  explicit

ext-implicit : {{ex : Extensionality}}  {A : Set}  {B : SetΠ A}  {f g : {a : A}  B a}  ({a : A}  f {a}  g {a})  _≡_ {_} { {a : A}  B a } f g
ext-implicit {{ex}} = snd ex

function : {A : Set}  {B : SetΠ A}  {f g : Π A B}  f  g  {a : A}  f a  g a
function refl = refl

ext-func : {{ext : Extensionality}}  {A : Set}  {B : SetΠ A}  {f g : Π A B}  f  g  ((a : A)  f a  g a)
ext-func =  eq _  function eq) , ext

ext-comp : {{ex : Extensionality}}  {B C : Set}  (f g : B  C)  f  g  ({A : Set}  (h : A  B)  f  h  g  h)
ext-comp f g eq h = ext' (function eq)