Wednesday 18 February 2009

Universes for discrimination proofs

I can't decide if this is trivial or not. What does this construction mean/say?


module Universe where

data N0 : Set where

data Bool : Set where
True : Bool
False : Bool

data Direction : Set where
Left : Direction
Right : Direction

data Eq (T : Set) : T -> T -> Set where
refl : (t : T) -> Eq T t t

-- Eq Set Bool Direction -> N0
-- is not provable
-- (techincally I would have to define Eq in Set1 but we can pretend universe polymorphism)

mutual
data U : Set where
n0 : U
bool : U
direction : U
eq : (A : U) -> T A -> T A -> U
pi : (A : U) -> (B : T A -> U) -> U

T : U -> Set
T n0 = N0
T bool = Bool
T direction = Direction
T (eq A x y) = Eq (T A) x y
T (pi A B) = (a : T A) -> T (B a)

mutual
data U1 : Set where
n0' : U1
bool' : U1
direction' : U1
eq' : (A : U1) -> T1 A -> T1 A -> U1
pi' : (A : U1) -> (B : T1 A -> U1) -> U1
u' : U1
lift : U -> U1

T1 : U1 -> Set
T1 n0' = N0
T1 bool' = Bool
T1 direction' = Direction
T1 (eq' A x y) = Eq (T1 A) x y
T1 (pi' A B) = (a : T1 A) -> T1 (B a)
T1 u' = U
T1 (lift A) = T A

T' : U -> Set
T' n0 = T n0
T' bool = T bool
T' direction = T n0
T' (eq A x y) = T n0
T' (pi A B) = T n0

rew : forall {A B : U} -> Eq U A B -> T' A -> T' B
rew (refl _) prf = prf

discr : Eq U bool direction -> N0
discr prf = rew prf True

corr : T1 (pi' (eq' u' bool direction) \_ -> n0')
corr = discr

No comments: