?. , ?. , and =. ,

, We prove the result above by induction on t. Most cases follow easily by induction hypotheses. Here, for demonstration purposes we show the case for variables and (dependent) function types

?. , In this case, both Case 1 and Case 2 above follow by definition of the model

:. ?-t-=-?x, ?. , ?. , ?. , =. et al., We know by induction hypothesis that

?. , ?. , ?. , =. , ?. et al.,

, Given the above induction hypotheses, both Case 1 and Case 2 above follow by the definition of the model

, Let ? be a typing context, ? be an environment, u and A be terms such that ? ?, ? ? ? and ? u ? ?. Then 1. If ?, x : A, ? ? and ?

?. If, :. , ?. , ?. , :. et al.,

, + size(t) ? 1 /2. In the following we reason as though we are conducting induction on the structure of terms and contexts. Note that this is allowed because our measure ?(?, t) does decrease for the induction hypotheses pertaining to structural induction, We prove this lemma by well-founded induction on ?(?, t) = size(?)

?. Case and ?. , Case 2, follows by induction on t. The only non-trivial case (not immediately following from the induction hypothesis) is the case where t is a variable, then Case 1 holds trivially

?. Case, ?. , and :. ,

, Notice, when z = x then both 2a and 2b hold trivially by definition of the model. Otherwise, we have to show that ?

?. Inria and . Case, Cum-trans: trivial by definition and induction hypothesis

?. Case, Cum-weaken: trivial by definition

C. ?-case, Prod: trivial by definition and induction hypothesis

, ? Case Cum-eq-L: trivial by definition and induction hypothesis

, ? Case Cum-eq-R: trivial by definition and induction hypothesis

, ? Case Cum: trivial by definition and induction hypothesis

, ? Case Cum-eq: trivial by definition and induction hypothesis

, ? Case Eq-Cum: trivial by definition and induction hypothesis

?. Case and C. ,

. ?-case-ind-eq,

C. ?-case, Eq-L: by definition

C. ?-case, Eq-R: by definition

, Let s be a sort, then, there does not exist any term t such that · t : ?x : s. x

A. Abel, Irrelevance in Type Theory with a Heterogeneous Equality Judgement, pp.57-71, 2011.

P. Aczel, An introduction to inductive definitions, Studies in Logic and the Foundations of Mathematics, vol.90, pp.739-782, 1977.

P. Aczel, On relating type theories and set theories, Types for Proofs and Programs: International Workshop, TYPES' 98, pp.1-18, 1998.

B. Barras, Semantical investigation in intuitionistic set theory and type theoris with inductive families, 2012.

F. R. Drake, Set theory : an introduction to large cardinals. Studies in logic and the foundations of mathematics 76, 1974.

P. Dybjer, Inductive Sets and Families in Martin-Löf's Type Theory and Their Set-Theoretic Semantics, pp.280-306, 1991.

M. Gitik, All uncountable cardinals can be singular, Israel Journal of Mathematics, vol.35, issue.1, pp.61-88, 1980.

G. Lee and B. Werner, Proof-irrelevant model of CC with predicative induction and judgmental equality, Logical Methods in Computer Science, vol.7, issue.4, 2011.

A. Miquel and B. Werner, The Not So Simple Proof-Irrelevant Model of CC, pp.240-258

H. Springer-berlin, , 2003.

T. Streicher, Investigations into intensional type theory, 1993.

, The Coq Development Team. The coq proof assistant, version 8.7+beta2, 2017.

A. Timany and B. Jacobs, First steps towards cumulative inductive types in CIC, Theoretical Aspects of Computing -ICTAC 2015, Proceedings, pp.608-617, 2015.

B. Werner, Sets in types, types in sets, Theoretical Aspects of Computer Software: Third International Symposium, TACS'97, pp.530-546, 1997.