ill-data-modal-tope-field.rzk

#lang rzk-1

-- A field of a modal tope kind would store a tope-layer citizen, seen
-- through a modality, inside type-layer data. The modal kinds are
-- parameters only.
#data F := c (psi : _op TOPE)