rzk-0.11.4: test/typecheck/cases/ill-kind-sigma-cube-universe.rzk
#lang rzk-1 -- The cube universe cannot be a Σ component. #define A : U := Σ (I : CUBE) , Unit
#lang rzk-1 -- The cube universe cannot be a Σ component. #define A : U := Σ (I : CUBE) , Unit