A. Abel, Irrelevance in Type Theory with a Heterogeneous Equality Judgement, pp.57-71978, 2011.
DOI : 10.2168/LMCS-4(3:13)2008

P. Aczel, An Introduction to Inductive Definitions, Studies in Logic and the Foundations of Mathematics, vol.90, pp.739-782, 1977.
DOI : 10.1016/S0049-237X(08)71120-0

P. Aczel, On Relating Type Theories and Set Theories, Types for Proofs and Programs: International Workshop, TYPES' 98 Kloster Irsee Selected Papers, pp.1-18, 1998.
DOI : 10.1007/3-540-48167-2_1

URL : http://www.cs.man.ac.uk/~petera/ts-st.ps.gz

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.
DOI : 10.1017/cbo9780511569807.012

M. Gitik, All uncountable cardinals can be singular, Israel Journal of Mathematics, vol.3, issue.1-2, pp.61-88, 1980.
DOI : 10.1007/BFb0061131

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, pp.2168-2175, 2011.
DOI : 10.2168/LMCS-4(3:13)2008

A. Miquel and B. Werner, The Not So Simple Proof-Irrelevant Model of CC, pp.240-258
DOI : 10.1007/3-540-39185-1_14

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

A. Timany and B. Jacobs, First Steps Towards Cumulative Inductive Types in CIC, Theoretical Aspects of Computing -ICTAC 2015, Proceedings, pp.608-617, 2015.
DOI : 10.1007/978-3-319-25150-9_36

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