module test where

Id : (A : U) (a b : A) -> U
Id = PN

refl : (A : U) (a : A) -> Id A a a
refl = PN

Bool : U
data Bool = true | false

orBool : Bool -> Bool -> Bool
orBool = split
  true -> \x -> true
  false -> \x -> x

id : Bool -> Bool
id x = x

test : Id Bool true (orBool true false)
test = refl Bool true