bib

all.bib

@@ -23389,11 +23389,15 @@ @Article{pare:comp-mod
   number =    16,
   pages =     {393--444}}
 
-@Unpublished{shulman:derex,
+@Article{shulman:derex,
   author =       {Michael Shulman},
   title =        {The derivator of setoids},
   note =         {arXiv:2105.08152},
-  year =      2021}
+  journal =      {Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle Cat\'egoriques},
+  year =         2023,
+  volume =    {LXIV},
+  number =    1,
+  pages =     {29--96}}
 
 @Misc{bakovic:fib-bicat,
   author =       {Igor Bakovi\'{c}},
@@ -23923,7 +23927,7 @@ @article{ctw:rew
 keywords = {termination, confluence, rewriting theory, dependent types, type theory}
 }
 
-@article{gknb:mmt,
+@article{gknb:mtt,
   TITLE = {Multimodal Dependent Type Theory},
   AUTHOR = {Daniel Gratzer and G. A. Kavvos and Andreas Nuyts and Lars Birkedal},
   URL = {https://lmcs.episciences.org/7713},
@@ -23952,7 +23956,7 @@ @article{sh:lrt
   volume = {68},
 }
 
-@article{gckgb:modal-pra,
+@article{gckgb:fitchtt,
 author = {Gratzer, Daniel and Cavallo, Evan and Kavvos, G. A. and Guatto, Adrien and Birkedal, Lars},
 title = {Modalities and Parametric Adjoints},
 year = {2022},
@@ -23998,3 +24002,88 @@ @article{shulman:lcm
   author={Shulman, Michael},
   year={2022},
   pages={327--386}}
+
+@Article{voevodsky:origins,
+  author =       {Vladimir Voevodsky},
+  note =         {\url{https://www.ias.edu/ideas/2014/voevodsky-origins}},
+  title =        {The Origins and Motivations of Univalent Foundations: A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes},
+  journal =      {The Institute Letter},
+  year =         2014}
+
+@Article{dpp:undecidable-free-adjoint,
+  author =       {Dawson, R.J.M. and Par\'{e}, R. and Pronk, D.A.},
+  title =        {Undecidability of the Free Adjoint Construction},
+  journal =      {Applied Categorical Structures},
+  year =         2003,
+  volume =    11,
+  pages =     {403--419},
+  doi =          {10.1023/A:1025712521140}}
+
+@inproceedings{nd:deg-rel,
+author = {Nuyts, Andreas and Devriese, Dominique},
+title = {Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory},
+year = {2018},
+isbn = {9781450355834},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/3209108.3209119},
+doi = {10.1145/3209108.3209119},
+booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
+pages = {779–788},
+numpages = {10},
+keywords = {unions, intersections, presheaf semantics, Parametricity, cubical type theory, erasure, irrelevance, algebra in type theory},
+location = {Oxford, United Kingdom},
+series = {LICS '18}
+}
+
+@article{nvd:parametric-quant,
+author = {Nuyts, Andreas and Vezzosi, Andrea and Devriese, Dominique},
+title = {Parametric Quantifiers for Dependent Type Theory},
+year = {2017},
+issue_date = {September 2017},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {1},
+number = {ICFP},
+url = {https://doi.org/10.1145/3110276},
+doi = {10.1145/3110276},
+journal = {Proc. ACM Program. Lang.},
+month = {aug},
+articleno = {32},
+numpages = {29},
+keywords = {presheaf semantics, Agda, cubical type theory, sized types, Parametricity}
+}
+
+@MISC {lax-dinat,
+    TITLE = {Which direction does a lax dinatural transformation go?},
+    AUTHOR = {S.C.\phantom{x}(https://mathoverflow.net/users/178774/s-c)},
+    HOWPUBLISHED = {MathOverflow},
+    NOTE = {URL:https://mathoverflow.net/q/438361 (version: 2023-01-12)},
+    EPRINT = {https://mathoverflow.net/q/438361},
+    URL = {https://mathoverflow.net/q/438361},
+  year =         2023
+}
+
+@misc{myers:orbifolds-sdchott,
+Author = {Myers, David Jaz},
+Title = {Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory},
+Year = {2022},
+Eprint = {arXiv:2205.15887},
+note = {arXiv:2205.15887},
+}
+
+@misc{ss:prop-orb-cohom,
+Author = {Hisham Sati and Urs Schreiber},
+Title = {Proper Orbifold Cohomology},
+Year = {2020},
+Eprint = {arXiv:2008.01101},
+note = {arXiv:2008.01101},
+}
+
+@Misc{glnprsw:dctt,
+  author =    {Jacob A. Gross, Daniel R. Licata, Max S. New, Jennifer Paykin, Mitchell Riley, Michael Shulman and Felix Wellen},
+  title =     {Differential Cohesive Type Theory (Extended Abstract))},
+  howpublished = {Workshop on Homotopy Type Theory and Univalent Foundations},
+  year =      2017,
+  note =      {\url{https://hott-uf.github.io/2017/}}}
+