From 519cc4779abf8f15f820e13acd006889287fea24 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 2 Jun 2024 17:34:08 +0200
Subject: [PATCH] add xtt2 and hofmann's quotient types to bib

---
 quox.bib | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/quox.bib b/quox.bib
index 25412e6..5c2ca0a 100644
--- a/quox.bib
+++ b/quox.bib
@@ -221,6 +221,17 @@
   doi       = {10.4230/LIPIcs.FSCD.2019.31}
 }
 
+@article{xtt2,
+  author  = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
+  title   = {A Cubical Language for Bishop Sets},
+  journal = {Log. Methods Comput. Sci.},
+  volume  = {18},
+  number  = {1},
+  year    = {2022},
+  url     = {https://doi.org/10.46298/lmcs-18(1:43)2022},
+  doi     = {10.46298/LMCS-18(1:43)2022},
+}
+
 @unpublished{cubical-ott,
   author = {James Chapman and Fredrik Nordvall Forsberg and Conor {McBride}},
   title  = {The Box of Delights (Cubical Observational Type Theory)},
@@ -456,6 +467,24 @@
 
 % Misc type stuff {{{1
 
+% not open access. i cry
+@inproceedings{simple-quotient,
+  author       = {Martin Hofmann},
+  editor       = {Mariangiola Dezani{-}Ciancaglini and Gordon D. Plotkin},
+  title        = {A Simple Model for Quotient Types},
+  booktitle    = {Typed Lambda Calculi and Applications,
+                  Second International Conference on Typed Lambda Calculi and
+                  Applications, {TLCA} '95, Edinburgh, UK, April 10-12, 1995,
+                  Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {902},
+  pages        = {216--234},
+  publisher    = {Springer},
+  year         = {1995},
+  url          = {https://doi.org/10.1007/BFb0014055},
+  doi          = {10.1007/BFB0014055},
+}
+
 @inproceedings{local,
   author    = {Michael Vollmer and
                Chaitanya Koparkar and