5
magic : {X : Set} -> FF -> X
10
data Id {S : Set}(s : S) : S -> Set where
17
all : (S : Set) -> (S -> Pr) -> Pr
18
_eq_ : {S : Set} -> S -> S -> Pr
20
record Sig (S : Set)(T : S -> Set) : Set where
25
open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T} public
27
_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sig S T
28
s , t = record {fst = s ; snd = t}
33
[| P /\ Q |] = Sig [| P |] \_ -> [| Q |]
34
[| all S P |] = (x : S) -> [| P x |]
38
P => Q = all [| P |] \_ -> Q
43
data Decision (P : Pr) : Set where
44
yes : [| P |] -> Decision P
45
no : [| ∼ P |] -> Decision P
59
so : (b : Bool) -> Decision (So b)
63
potahto : (b : Bool) -> [| So (not b) => ∼ (So b) |]
67
PEx : (P : Pr) -> ([| P |] -> Pr) -> Pr
68
PEx P Q = P /\ all [| P |] Q
73
_==>_ : {X : Set} -> Pow X -> Pow X -> Pr
74
_==>_ {X} P Q = all X \x -> P x => Q x
76
Decidable : {X : Set}(P : Pow X) -> Set
77
Decidable {X} P = (x : X) -> Decision (P x)
79
data _:-_ (S : Set)(P : Pow S) : Set where
80
[_/_] : (s : S) -> [| P s |] -> S :- P
82
wit : {S : Set}{P : S -> Pr} -> S :- P -> S
85
cert : {S : Set}{P : S -> Pr}(sp : S :- P) -> [| P (wit sp) |]
88
_??_ : {S : Set}{P : S -> Pr}
89
(sp : S :- P){M : Set} ->
90
((s : S)(p : [| P s |]) -> M) ->
92
sp ?? m = m (wit sp) (cert sp)