Pr.agda

module Pr where

data FF : Set where

magic : {X : Set} -> FF -> X
magic ()

record TT : Set where

data Id {S : Set}(s : S) : S -> Set where
  refl : Id s s

data Pr : Set1 where
  tt : Pr
  ff : Pr
  _/\_ : Pr -> Pr -> Pr
  all : (S : Set) -> (S -> Pr) -> Pr
  _eq_ : {S : Set} -> S -> S -> Pr

record Sig (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T} public

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sig S T
s , t = record {fst = s ; snd = t}

[|_|] : Pr -> Set
[| tt |] = TT
[| ff |] = FF
[| P /\ Q |] = Sig [| P |] \_ -> [| Q |]
[| all S P |] = (x : S) -> [| P x |]
[| a eq b |] = Id a b

_=>_ : Pr -> Pr -> Pr
P => Q = all [| P |] \_ -> Q

∼ : Pr -> Pr
∼ P = P => ff

data Decision (P : Pr) : Set where
  yes  : [| P |]   -> Decision P
  no   : [| ∼ P |] -> Decision P

data Bool : Set where
  true : Bool
  false : Bool

So : Bool -> Pr
So true = tt
So false = ff

not : Bool -> Bool
not true = false
not false = true

so : (b : Bool) -> Decision (So b)
so true = yes _
so false = no magic

potahto : (b : Bool) -> [| So (not b) => ∼ (So b) |]
potahto true () _
potahto false _ ()

PEx : (P : Pr) -> ([| P |] -> Pr) -> Pr
PEx P Q = P /\ all [| P |] Q

Pow : Set -> Set1
Pow X = X -> Pr

_==>_ : {X : Set} -> Pow X -> Pow X -> Pr
_==>_ {X} P Q = all X \x -> P x => Q x

Decidable : {X : Set}(P : Pow X) -> Set
Decidable {X} P = (x : X) -> Decision (P x)

data _:-_ (S : Set)(P : Pow S) : Set where
  [_/_] : (s : S) -> [| P s |] -> S :- P

wit : {S : Set}{P : S -> Pr} -> S :- P -> S
wit [ s / p ] = s

cert : {S : Set}{P : S -> Pr}(sp : S :- P) -> [| P (wit sp) |]
cert [ s / p ] = p

_??_ : {S : Set}{P : S -> Pr}
      (sp : S :- P){M : Set} ->
      ((s : S)(p : [| P s |]) -> M) ->
      M
sp ?? m = m (wit sp) (cert sp)