## 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 wheredata N0 : Set wheredata Bool : Set where True : Bool False : Booldata Direction : Set where Left : Direction Right : Directiondata 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 AT' : U -> SetT' n0 = T n0T' bool = T boolT' direction = T n0T' (eq A x y) = T n0T' (pi A B) = T n0rew : forall {A B : U} -> Eq U A B -> T' A -> T' Brew (refl _) prf = prfdiscr : Eq U bool direction -> N0discr prf = rew prf Truecorr : T1 (pi' (eq' u' bool direction) \_ -> n0')corr = discr`