foo.idr

%default total

data Two : Type where
  TT : Two
  FF : Two

So : Two -> Type
So TT = ()
So FF = Void

-- I don't think this reflects agda's use of {{ }}
data Prop : Type -> Type where
  Bang : {prf : p} -> Prop p

-- This similarily doesn't seem quite right
infixr 3 :=>
(:=>) : Type -> Type -> Type
(:=>) p t = {auto pe : p} -> t

tripleDot : Prop p -> (p :=> t) -> t
tripleDot (Bang {prf}) y = y prf

magic : {x : Type} -> Void :=> x
magic = absurd

Nawt : Two -> Two
Nawt TT = FF
Nawt FF = TT

-- I need to provide () and Void here but the agda version just uses x or y
if_then_else_ : {x : Type} -> (b : Two) -> (So b :=> x) -> (So (Nawt b) :=> x) -> x
if_then_else_ TT x y = ?dfs
if_then_else_ FF x y = ?ffewf