4 lines (3 loc) · 206 Bytes

cic-model

Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization