Irrelevance in Type Theory with a Heterogeneous Equality Judgement, pp.57-71978, 2011. ,
DOI : 10.2168/LMCS-4(3:13)2008
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
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
Semantical investigation in intuitionistic set theory and type theoris with inductive families, 2012 ,
Set theory : an introduction to large cardinals. Studies in logic and the foundations of mathematics 76, 1974. ,
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
All uncountable cardinals can be singular, Israel Journal of Mathematics, vol.3, issue.1-2, pp.61-88, 1980. ,
DOI : 10.1007/BFb0061131
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
The Not So Simple Proof-Irrelevant Model of CC, pp.240-258 ,
DOI : 10.1007/3-540-39185-1_14
Investigations into intensional type theory, 1993. ,
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
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