0 | module BeTTI.FunExt
 1 |
 2 | import System
 3 | import System.File
 4 |
 5 | %default total
 6 |
 7 | public export 0
 8 | FunExt : (f,g : a -> b) -> Type
 9 | FunExt f g = (x : a) -> f x = g x
10 |
11 | export 0
12 | funext : (f,g : a -> b) -> FunExt f g -> f = g
13 | funext f g prf = believe_me $ unsafePerformIO (do
14 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
15 |      exitWith {a = f = g} $ ExitFailure 1)
16 |
17 | public export 0
18 | FunExt0 : (f,g : (0 x :a) -> b) -> Type
19 | FunExt0 f g = (x : a) -> f x = g x
20 |
21 |
22 | export 0
23 | funext0 : (f,g : (0 x : a) -> b) -> FunExt0 f g -> f = g
24 | funext0 f g prf = believe_me $ unsafePerformIO (do
25 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
26 |      exitWith {a = f = g} $ ExitFailure 1)
27 |
28 | public export 0
29 | DepFunExt : (b : a -> Type) -> (f,g : (x : a) -> b x) -> Type
30 | DepFunExt b f g = (x : a) -> f x = g x
31 |
32 | export 0
33 | depfunext : (b : a -> Type) -> (f,g : (x : a) -> b x) -> DepFunExt b f g -> f = g
34 | depfunext b f g prf = believe_me $ unsafePerformIO (do
35 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
36 |      exitWith {a = f = g} $ ExitFailure 1)
37 |
38 | public export 0
39 | DepFunExtI : (b : a -> Type) -> (f,g : {x : a} -> b x) -> Type
40 | DepFunExtI b f g = (x : a) -> f {x} = g {x}
41 |
42 | export 0
43 | depfunexti : (b : a -> Type) -> (f,g : {x : a} -> b x) ->
44 |   DepFunExtI b f g -> Equal f g {a = {x : a} -> b x}
45 | depfunexti b f g prf =
46 |      -- get around Idris feature request #14 and the issues mentioned therein
47 |      let 0 result : Type
48 |          result = ?
49 |      in the result $ believe_me $ the (IO result) $ unsafePerformIO (do
50 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
51 |      exitWith $ ExitFailure 1)
52 |
53 | public export 0
54 | DepFunExt0 : (b : a -> Type) -> (f,g : (0 x : a) -> b x) -> Type
55 | DepFunExt0 b f g = (x : a) -> f x = g x
56 |
57 |
58 | export 0
59 | depfunext0 : (b : a -> Type) -> (f,g : (0 x : a) -> b x) -> DepFunExt0 b f g -> f = g
60 | depfunext0 b f g prf = believe_me $ unsafePerformIO (do
61 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
62 |      exitWith {a = f = g} $ ExitFailure 1)
63 |
64 |
65 | export 0
66 | depcurryfunext : (b : a -> Type) -> (c : (x : a) -> b x -> Type) ->
67 |   (f,g : (x :a) -> (y : b x) -> c x y) ->
68 |   DepFunExt {a = DPair a b}
69 |              (\(x ** y) => c x y)
70 |              (\(x ** y) => f x y)
71 |              (\(x ** y) => g x y) -> f = g
72 | depcurryfunext b c f g prf =
73 |   depfunext (\x => (y : b x) -> c x y) f g $ \x =>
74 |   depfunext (\y => c x y) (f x) (g x) $ \y => prf (x ** y)
75 |