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, Thorsten Altenkirch, Bernhard Reus, and Wolfgang Naraschewski, pp.1-18, 1999.

B. Barras, Semantical Investigation in Intuitionistic Set Theory and Type Theoris with Inductive Families, 2012.

S. Boulier, P. Pédrot, and N. Tabareau, The Next 700 Syntactical Models of Type Theory, CPP 2017, pp.182-194, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01445835

. Frank-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 SetTheoretic Semantics, pp.280-306, 1991.

J. Girard, Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972.

R. Harper and R. Pollack, Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft, TAPSOFT '89, pp.241-256, 1989.

J. C. Antonius and . Hurkens, A simplification of Girard's paradox, International Conference on Typed Lambda Calculi and Applications, pp.266-278, 1995.

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.

C. Mcbride, Universe hierarchies, 2015.

C. Paulin-mohring, Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitation à diriger les recherches, 1996.

D. Rouhling, Dependently typed lambda calculus with a lifting operator, 2014.

V. Siles and H. Herbelin, Pure type system conversion is always typable, J. Funct. Program, vol.22, issue.2, pp.153-180, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00497177

M. Sozeau and N. Tabareau, Universe Polymorphism in Coq, Interactive Theorem Proving, pp.499-514, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00974721

, The Coq Development Team. The Coq Proof Assistant, 2017.

A. Timany and B. Jacobs, First Steps Towards Cumulative Inductive Types in CIC, Theoretical Aspects of Computing, pp.608-617, 2015.

A. Timany and B. Jacobs, Category Theory in Coq 8.5. In Formal Structures for Computation and Deduction, vol.30, 2016.

A. Timany and M. Sozeau, Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC), KU Leuven, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01615123