4 lines
220 B
Agda
4 lines
220 B
Agda
module Preliminaries where
|
||
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) public
|
||
postulate
|
||
FunExt : ∀ {ℓ} {X Y : Set ℓ} {f g : X → Y} → (∀ (x : X) → f x ≡ g x) → f ≡ g
|