--- a/latex/cpdt.bib	Thu Nov 03 17:04:41 2011 -0400
+++ b/latex/cpdt.bib	Sun Nov 06 16:25:45 2011 -0500
@@ -309,3 +309,19 @@
   booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
   year      = {1997},
 }
+
+@inproceedings{JMeq,
+  author = {McBride, Conor},
+  title = {Elimination with a Motive},
+  booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs},
+  year = {2000},
+  pages = {197--216}
+}
+
+@phdthesis{AxiomK,
+  author = {Thomas Streicher},
+  title = {Semantical Investigations into Intensional Type Theory},
+  type = {Habilitationsschrift},
+  school = {LMU M\"unchen},
+  year= {1993}
+}