ill-kind-sigma-tope.rzk

#lang rzk-1

-- The tope universe cannot be a Σ component: it would store topes as data.
#define A : U := Σ (p : TOPE) , Unit