@article(Thorsten,
 author       = {Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus},
 year         = {2016},
 title        = {Extending Homotopy Type Theory with Strict Equality},
 doi          = {10.4230/LIPIcs.CSL.2016.21},
)
@inproceedings(RedPRL,
 author       = {Carlo Angiuli and Kuen{-}Bang~Hou (Favonia) and Robert Harper},
 year         = {2018},
 title        = {Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities},
 editor       = {Dan~R. Ghica and Achim Jung},
 booktitle    = {27th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2018, September 4-7, 2018, Birmingham, {UK}},
 series       = {LIPIcs},
 volume       = {119},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {6:1--6:17},
 doi          = {10.4230/LIPIcs.CSL.2018.6},
)
@misc(Danil,
 author       = {Danil Annenkov and Paolo Capriotti and Nicolai Kraus and Christian Sattler},
 year         = {2017},
 title        = {Two-Level Type Theory and Applications},
)
@inproceedings(assaf-completeness,
 author       = {Ali Assaf},
 year         = {2015},
 title        = {Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting},
 editor       = {Thorsten Altenkirch},
 booktitle    = {13th International Conference on Typed Lambda Calculi and Applications, {TLCA} 2015, July 1-3, 2015, Warsaw, Poland},
 series       = {LIPIcs},
 volume       = {38},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {31--44},
 doi          = {10.4230/LIPIcs.TLCA.2015.31},
)
@article(assaf,
 author       = {Ali Assaf and Guillaume Burel and Rapha{\"e}l Cauderlier and David Delahaye and Gilles Dowek and Catherine Dubois and Fr{\'e}d{\'e}ric Gilbert and Pierre Halmagrand and Olivier Hermant and Ronan Saillard},
 year         = {2016},
 title        = {Dedukti: a logical framework based on the $\lambda$$\Pi$-calculus modulo theory},
 journal      = {Unpublished manuscript},
 url          = {http://www.lsv.fr/~dowek/Publi/expressing.pdf},
)
@inproceedings(CoqMTU,
 author       = {Bruno Barras and Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub and Qian Wang},
 year         = {2011},
 title        = {CoQMTU: {A} Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory},
 booktitle    = {Proceedings of the 26th Annual {IEEE} Symposium on Logic in Computer Science, {LICS} 2011, June 21-24, 2011, Toronto, Ontario, Canada},
 publisher    = {{IEEE} Computer Society},
 pages        = {143--151},
 doi          = {10.1109/LICS.2011.37},
)
@misc(CCHM,
 author       = {Cyril Cohen and Thierry Coquand and Simon Huber and M\IeC{\"o}rtberg, Anders},
 year         = {2016},
 title        = {Cubical Type Theory: a constructive interpretation of the univalence axiom},
)
@misc(MLTT,
 author       = {Martin Hofmann},
 year         = {1997},
 title        = {Syntax and semantics of dependent types},
)
@book(HottBook,
 author       = {{Univalent Foundations Program}, The},
 year         = {2013},
 title        = {Homotopy Type Theory: Univalent Foundations of Mathematics},
 publisher    = {\url{https://homotopytypetheory.org/book}},
 address      = {Institute for Advanced Study},
)
@inproceedings(ExtensionalTT,
 author       = {Th{\'{e}}o Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
 year         = {2019},
 title        = {Eliminating reflection from type theory},
 editor       = {Assia Mahboubi and Magnus~O. Myreen},
 booktitle    = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January 14-15, 2019},
 publisher    = {{ACM}},
 pages        = {91--103},
 doi          = {10.1145/3293880.3294095},
)