5 lines
220 B
Agda
5 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
|