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