References

  1. M. Abbott, T. Altenkirch & N. Ghani (2005): Containers: Constructing Strictly Positive Types. Theoretical Computer Science 342(1), pp. 3–27, doi:10.1016/j.tcs.2005.06.002.
  2. A. Abel (2012): Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types. Electronic Proceedings in Theoretical Computer Science 77, pp. 1–11, doi:10.4204/EPTCS.77.1.
  3. A. Abel & B. Pientka (2016): Well-Founded Recursion with Copatterns and Sized Types. Journal of Functional Programming 26, pp. 61, doi:10.1017/S0956796816000022.
  4. J. Adámek (1974): Free Algebras and Automata Realizations in the Language of Categories. Commentationes Mathematicae Universitatis Carolinae 15(4), pp. 589–602.
  5. J. Adámek, S. Milius & L. S. Moss (2021): An Initial Algebra Theorem Without Iteration. ArXiv e-prints arXiv:2104.09837 [cs.LO]. Available at https://arxiv.org/abs/2104.09837.
  6. J. Adámek, S. Milius & L. S. Moss (2021): Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors. Available at http://www.stefan-milius.eu. Draft book.
  7. J. Adámek & J. Rosický (1994): Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, doi:10.1017/CBO9780511600579.
  8. Agda v2.6.1 (2021). Available at https://agda.readthedocs.io/en/v2.6.1.3/index.html.
  9. T. Altenkirch, P. Capriotti, G. Dijkstra, N. Kraus & F. N. Forsberg (2018): Quotient Inductive-Inductive Types. In: C. Baier & U. Dal Lago: Foundations of Software Science and Computation Structures, FoSSaCS 2018, Lecture Notes in Computer Science 10803. Springer International Publishing, pp. 293–310, doi:10.1007/978-3-319-89366-2_16.
  10. A Bauer & P. Lumsdaine (2013): On the BourbakiWitt Principle in Toposes. Mathematical Proceedings of the Cambridge Philosophical Society 155(1), pp. 87–99, doi:10.1017/S0305004113000108.
  11. P. Dybjer (2000): A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65(2), pp. 525–549, doi:10.1305/ndjfl/1093635159.
  12. M. P. Fiore & C.-K. Hur (2008): On the Construction of Free Algebras for Equational Systems. Theoretical Computer Science 410, pp. 1704–1729, doi:10.1016/j.tcs.2008.12.052.
  13. M. P. Fiore, A. M. Pitts & S. C. Steenkamp (2020): Constructing Infinitary Quotient-Inductive Types. In: J. Goubault-Larrecq & B. König: 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), Lecture Notes in Computer Science 12077. Springer, pp. 257–276, doi:10.1007/978-3-030-45231-5_14.
  14. M. P. Fiore, A. M. Pitts & S. C. Steenkamp (2021): Quotients, Inductive Types and Quotient Inductive Types. ArXiv e-prints arXiv:2101.02994 [cs.LO]. Available at https://arxiv.org/abs/2101.02994.
  15. F. N. Forsberg (2013): Inductive-Inductive Definitions. Swansea University.
  16. N. Gambino & M. Hyland (2004): Wellfounded Trees and Dependent Polynomial Functors. In: S. Berardi, M. Coppo & F. Damiani: Types for Proofs and Programs, Lecture Notes in Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 210–225, doi:10.1007/978-3-540-24849-1_14.
  17. H. R. Gylterud (2011): Symmetric Containers. Master of Science. Department of Mathematics, University of Oslo. Available at https://www.duo.uio.no/bitstream/handle/10852/10740/thesisgylterud.pdf.
  18. P. T. Johnstone (2002): Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2. Oxford Logic Guides 43–44. Oxford University Press.
  19. A. Kovács & A. Kaposi (2020): Large and Infinitary Quotient Inductive-Inductive Types. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20. Association for Computing Machinery, New York, NY, USA, pp. 648661, doi:10.1145/3373718.3394770.
  20. P. B. Levy (2021): Broad Infinity and Generation Principles. ArXiv e-prints arXiv:2101.01698 [math.LO]. Available at https://arxiv.org/abs/2101.01698.
  21. D. R. Licata, I. Orton, A. M. Pitts & B. Spitters (2018): Internal Universes in Models of Homotopy Type Theory. In: H. Kirchner: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs) 108. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 22:1–22:17, doi:10.4230/LIPIcs.FSCD.2018.22.
  22. P. Martin-Löf (1984): Intuitionistic Type Theory. Bibliopolis, Napoli.
  23. E. Meijer, M. Fokkinga & R. Paterson (1991): Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. In: J. Hughes: Functional Programming Languages and Computer Architecture, FPCA 1991, Lecture Notes in Computer Science 523. Springer, Berlin, Heidelberg, pp. 124–144, doi:10.1007/3540543961_7.
  24. I. Moerdijk & E. Palmgren (2000): Wellfounded Trees in Categories. Annals of Pure and Applied Logic 104(1), pp. 189–218, doi:10.1016/S0168-0072(00)00012-9.
  25. I. Moerdijk & E. Palmgren (2002): Type theories, Toposes and Constructive Set Theory: Predicative Aspects of AST. Annals of Pure and Applied Logic 114(1), pp. 155–201, doi:10.1016/S0168-0072(01)00079-3.
  26. B. Nordström, K. Petersson & J. M. Smith (1990): Programming in Martin-Löf's Type Theory. Oxford University Press.
  27. I. Orton & A. M. Pitts (2016): Axioms for Modelling Cubical Type Theory in a Topos. In: J.-M. Talbot & L. Regnier: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics (LIPIcs) 62. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 24:1–24:19, doi:10.4230/LIPIcs.CSL.2016.24.
  28. A. M. Pitts & S. C. Steenkamp (2021): Agda code accompanying this paper, doi:10.17863/CAM.73911.
  29. D. M. Roberts (2015): The Weak Choice Principle WISC may Fail in the Category of Sets. Studia Logica 103, pp. 1005–1017, doi:10.1007/s11225-015-9603-6.
  30. M. Shulman (2014): The surreals contain the plump ordinals. Available at https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/. Homotopy Type Theory blog.
  31. C. Sprenger & M. Dam (2003): On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μCalculus. In: A. D. Gordon: Foundations of Software Science and Computation Structures (FoSSaCS 2003), Lecture Notes in Computer Science 2620. Springer, Berlin, Heidelberg., pp. 425–440, doi:10.1007/3-540-36576-1_27.
  32. T. Streicher (2005): Realizability Models for CZF + Pow. Available at http://www2.mathematik.tu-darmstadt.de/~streicher/CIZF/rmczfnp.pdf. Unpublished note.
  33. T. Streicher (2005): Universes in Toposes. In: L. Crosilla & P. Schuster: From Sets and Types to Topology and Analysis, Towards Practicable Foundations for Constructive Mathematics, chapter 4, Oxford Logic Guides 48. Oxford University Press, pp. 78–90, doi:10.1093/acprof:oso/9780198566519.001.0001.
  34. A. Swan (2018): W-Types with Reductions and the Small Object Argument. ArXiv e-prints arXiv:1802.07588 [math.CT]. Available at https://arxiv.org/abs/1802.07588.
  35. P. Taylor (1996): Intuitionistic Sets and Ordinals. Journal of Symbolic Logic 61, pp. 705–744, doi:10.2307/2275781.
  36. P. Taylor (1999): Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics 59. Cambridge University Press.
  37. The Univalent Foundations Program (2013): Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study. Available at http://homotopytypetheory.org/book.
  38. B. van den Berg & I. Moerdijk (2014): The Axiom of Multiple Choice and Models for Constructive Set Theory. Journal of Mathematical Logic 14(01), pp. 1450005, doi:10.1142/S0219061314500056.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org