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