[ funext ] Add a proof for funext variants with the other quantities

idris-lang · May 19, 2024 · cf68e99 · cf68e99
1 parent 2a3f031
commit cf68e99
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
@@ -127,6 +127,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Removed need for the runtime value of the implicit argument in `succNotLTEpred`.
 
+* Added `funExt0` and `funExt1`, functions analogous to `funExt` but for functions
+  with quantities 0 and 1 respectively.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

diff --git a/libs/base/Control/Function/FunExt.idr b/libs/base/Control/Function/FunExt.idr
@@ -10,3 +10,11 @@ module Control.Function.FunExt
 public export
 interface FunExt where
   funExt : {0 b : a -> Type} -> {0 f, g : (x : a) -> b x} -> ((x : a) -> f x = g x) -> f = g
+
+export
+funExt0 : FunExt => {0 b : a -> Type} -> {0 f, g : (0 x : a) -> b x} -> ((x : a) -> f x = g x) -> f = g
+funExt0 prf = rewrite funExt {f = \x => f x} {g = \y => g y} prf in Refl
+
+export
+funExt1 : FunExt => {0 b : a -> Type} -> {0 f, g : (1 x : a) -> b x} -> ((x : a) -> f x = g x) -> f = g
+funExt1 prf = rewrite funExt {f = \x => f x} {g = \y => g y} prf in Refl