@inproceedings{10.1145/2837614.2837638,
    Abstract = {We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.},
    Address = {New York, NY, USA},
    Author = {Altenkirch, Thorsten and Kaposi, Ambrus},
    BookTitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
    File = {Type theory in type theory using quotient inductive types - tt-in-tt - a - u.pdf},
    ISBN = {9781450335492},
    Keywords = {Logical Relations, Metaprogramming, Higher Inductive Types, Homotopy Type Theory, Agda},
    Location = {St. Petersburg, FL, USA},
    Pages = {18--29},
    Publisher = {Association for Computing Machinery},
    Series = {POPL '16},
    Title = {Type Theory in Type Theory Using Quotient Inductive Types},
    URL = {https://doi.org/10.1145/2837614.2837638},
    Year = {2016},
    bdsk-url-1 = {https://doi.org/10.1145/2837614.2837638},
    date-added = {2020-09-25 19:51:07 +0200},
    date-modified = {2020-09-25 19:51:07 +0200},
    numpages = {12},
    doi = {10.1145/2837614.2837638}
}

@inproceedings{10.1145/2837614.2837638, Abstract = {We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.}, Address = {New York, NY, USA}, Author = {Altenkirch, Thorsten and Kaposi, Ambrus}, BookTitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, File = {Type theory in type theory using quotient inductive types - tt-in-tt - a - u.pdf}, ISBN = {9781450335492}, Keywords = {Logical Relations, Metaprogramming, Higher Inductive Types, Homotopy Type Theory, Agda}, Location = {St. Petersburg, FL, USA}, Pages = {18--29}, Publisher = {Association for Computing Machinery}, Series = {POPL '16}, Title = {Type Theory in Type Theory Using Quotient Inductive Types}, URL = {https://doi.org/10.1145/2837614.2837638}, Year = {2016}, bdsk-url-1 = {https://doi.org/10.1145/2837614.2837638}, date-added = {2020-09-25 19:51:07 +0200}, date-modified = {2020-09-25 19:51:07 +0200}, numpages = {12}, doi = {10.1145/2837614.2837638} }