Proof-irrelevant model of CC with predicative induction and judgmental equality

We present a set-theoretic, proof-irrelevant model for Calculus ofConstructions (CC) with predicative induction and judgmental equality inZermelo-Fraenkel set theory with an axiom for countably many inaccessiblecardinals. We use Aczel's trace encoding which is universally defined for anyfunction type, regardless of being impredicative. Direct and concreteinterpretations of simultaneous induction and mutually recursive functions arealso provided by extending Dybjer's interpretations on the basis of Aczel'srule sets. Our model can be regarded as a higher-order generalization of thetruth-table methods. We provide a relatively simple consistency proof of typetheory, which can be used as the basis for a theorem prover