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