@article(abbott2005containers,
 author       = {M.~Abbott and T.~Altenkirch and N.~Ghani},
 year         = {2005},
 title        = {Containers: Constructing Strictly Positive Types},
 journal      = {Theoretical Computer Science},
 volume       = {342},
 number       = {1},
 pages        = {3--27},
 doi          = {10.1016/j.tcs.2005.06.002},
)
@article(AbelA:typbti,
 author       = {A.~Abel},
 year         = {2012},
 title        = {Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {77},
 pages        = {1--11},
 doi          = {10.4204/EPTCS.77.1},
)
@article(AbelA:wellfrc,
 author       = {A.~Abel and B.~Pientka},
 year         = {2016},
 title        = {Well-Founded Recursion with Copatterns and Sized Types},
 journal      = {Journal of Functional Programming},
 volume       = {26},
 pages        = {61},
 doi          = {10.1017/S0956796816000022},
)
@article(AdamekJ:freaar,
 author       = {J.~Ad{\'a}mek},
 year         = {1974},
 title        = {Free Algebras and Automata Realizations in the Language of Categories},
 journal      = {Commentationes Mathematicae Universitatis Carolinae},
 volume       = {15},
 number       = {4},
 pages        = {589--602},
)
@article(AdamekJ:iniatw,
 author       = {J.~Ad{\'a}mek and S.~Milius and L.~S. Moss},
 year         = {2021},
 title        = {An Initial Algebra Theorem Without Iteration},
 journal      = {ArXiv e-prints},
 volume       = {arXiv:2104.09837 [cs.LO]},
 url          = {https://arxiv.org/abs/2104.09837},
)
@unpublished(ammbook,
 author       = {J.~Ad{\'a}mek and S.~Milius and L.~S. Moss},
 year         = {2021},
 title        = {Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors},
 url          = {http://www.stefan-milius.eu},
 note         = {Draft book},
)
@book(AdamekJ:locpac,
 author       = {J.~Ad{\'a}mek and J.~Rosick{\'y}},
 year         = {1994},
 title        = {Locally Presentable and Accessible Categories},
 series       = {London Mathematical Society Lecture Note Series},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511600579},
)
@misc(Agda261,
 author       = {{Agda v2.6.1}},
 year         = {2021},
 url          = {https://agda.readthedocs.io/en/v2.6.1.3/index.html},
)
@inproceedings(AltenkirchT:quoiit,
 author       = {T.~Altenkirch and P.~Capriotti and G.~Dijkstra and N.~Kraus and F.~N. Forsberg},
 year         = {2018},
 title        = {Quotient Inductive-Inductive Types},
 editor       = {C.~Baier and U.~Dal Lago},
 booktitle    = {Foundations of Software Science and Computation Structures, {FoSSaCS}~2018},
 series       = {Lecture Notes in Computer Science},
 volume       = {10803},
 publisher    = {Springer International Publishing},
 pages        = {293--310},
 doi          = {10.1007/978-3-319-89366-2{\_}16},
)
@article(BauerA:bouwpt,
 author       = {A~Bauer and P.~Lumsdaine},
 year         = {2013},
 title        = {On the Bourbaki\IeC{\textendash}Witt Principle in Toposes},
 journal      = {Mathematical Proceedings of the Cambridge Philosophical Society},
 volume       = {155},
 number       = {1},
 pages        = {87--99},
 doi          = {10.1017/S0305004113000108},
)
@article(DybjerP:genfsi,
 author       = {P.~Dybjer},
 year         = {2000},
 title        = {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory},
 journal      = {Journal of Symbolic Logic},
 volume       = {65},
 number       = {2},
 pages        = {525--549},
 doi          = {10.1305/ndjfl/1093635159},
)
@article(FioreMP:confae,
 author       = {M.~P. Fiore and C.-K. Hur},
 year         = {2008},
 title        = {On the Construction of Free Algebras for Equational Systems},
 journal      = {Theoretical Computer Science},
 volume       = {410},
 pages        = {1704--1729},
 doi          = {10.1016/j.tcs.2008.12.052},
)
@inproceedings(PittsAM:coniqi,
 author       = {M.~P. Fiore and A.~M. Pitts and S.~C. Steenkamp},
 year         = {2020},
 title        = {Constructing Infinitary Quotient-Inductive Types},
 editor       = {J.~Goubault-Larrecq and B.~K{\"o}nig},
 booktitle    = {23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020)},
 series       = {Lecture Notes in Computer Science},
 volume       = {12077},
 publisher    = {Springer},
 pages        = {257--276},
 doi          = {10.1007/978-3-030-45231-5_14},
)
@article(PittsAM:quoitq,
 author       = {M.~P. Fiore and A.~M. Pitts and S.~C. Steenkamp},
 year         = {2021},
 title        = {Quotients, Inductive Types and Quotient Inductive Types},
 journal      = {ArXiv e-prints},
 volume       = {arXiv:2101.02994 [cs.LO]},
 url          = {https://arxiv.org/abs/2101.02994},
)
@phdthesis(ForsbergFN:indid,
 author       = {F.~N. Forsberg},
 year         = {2013},
 title        = {Inductive-Inductive Definitions},
 school       = {Swansea University},
)
@inproceedings(GambinoN:welftd,
 author       = {N.~Gambino and M.~Hyland},
 year         = {2004},
 title        = {Wellfounded Trees and Dependent Polynomial Functors},
 editor       = {S.~Berardi and M.~Coppo and F.~Damiani},
 booktitle    = {Types for Proofs and Programs},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {210--225},
 doi          = {10.1007/978-3-540-24849-1{\_}14},
)
@mastersthesis(GylterudHR:symc,
 author       = {H.~R. Gylterud},
 year         = {2011},
 title        = {Symmetric Containers},
 type         = {Master of {S}cience},
 school       = {Department of Mathematics, University of Oslo},
 url          = {https://www.duo.uio.no/bitstream/handle/10852/10740/thesisgylterud.pdf},
)
@book(JohnstonePT:skeett,
 author       = {P.~T. Johnstone},
 year         = {2002},
 title        = {Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2},
 series       = {Oxford Logic Guides},
 volume       = {43--44},
 publisher    = {Oxford University Press},
)
@inproceedings(KaposiA:lariqi,
 author       = {A.~Kov\'{a}cs and A.~Kaposi},
 year         = {2020},
 title        = {Large and Infinitary Quotient Inductive-Inductive Types},
 booktitle    = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science},
 series       = {LICS '20},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {648\IeC{\textendash}661},
 doi          = {10.1145/3373718.3394770},
)
@article(LevyP:broigp,
 author       = {P.~B. Levy},
 year         = {2021},
 title        = {Broad Infinity and Generation Principles},
 journal      = {ArXiv e-prints},
 volume       = {arXiv:2101.01698 [math.LO]},
 url          = {https://arxiv.org/abs/2101.01698},
)
@inproceedings(PittsAM:intumh,
 author       = {D.~R. Licata and I.~Orton and A.~M. Pitts and B.~Spitters},
 year         = {2018},
 title        = {Internal Universes in Models of Homotopy Type Theory},
 editor       = {H.~Kirchner},
 booktitle    = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {108},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f\"ur Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {22:1--22:17},
 doi          = {10.4230/LIPIcs.FSCD.2018.22},
)
@book(Martin-LoefP:inttt,
 author       = {P.~{Martin-L\"of}},
 year         = {1984},
 title        = {Intuitionistic Type Theory},
 publisher    = {Bibliopolis, Napoli},
)
@inproceedings(MeijerE:funpbl,
 author       = {E.~Meijer and M.~Fokkinga and R.~Paterson},
 year         = {1991},
 title        = {Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire},
 editor       = {J.~Hughes},
 booktitle    = {Functional Programming Languages and Computer Architecture, {FPCA}~1991},
 series       = {Lecture Notes in Computer Science},
 volume       = {523},
 publisher    = {Springer, Berlin, Heidelberg},
 pages        = {124--144},
 doi          = {10.1007/3540543961{\_}7},
)
@article(MoerdijkI:weltc,
 author       = {I.~Moerdijk and E.~Palmgren},
 year         = {2000},
 title        = {Wellfounded Trees in Categories},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {104},
 number       = {1},
 pages        = {189--218},
 doi          = {10.1016/S0168-0072(00)00012-9},
)
@article(MoerdijkI:typttc,
 author       = {I.~Moerdijk and E.~Palmgren},
 year         = {2002},
 title        = {Type theories, Toposes and Constructive Set Theory: Predicative Aspects of {AST}},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {114},
 number       = {1},
 pages        = {155--201},
 doi          = {10.1016/S0168-0072(01)00079-3},
)
@book(NordstromB:progmlt,
 author       = {B.~Nordstr{\"o}m and K.~Petersson and J.~M. Smith},
 year         = {1990},
 title        = {Programming in {Martin-L{\"o}f's} Type Theory},
 publisher    = {Oxford University Press},
)
@inproceedings(PittsAM:aximct,
 author       = {I.~Orton and A.~M. Pitts},
 year         = {2016},
 title        = {Axioms for Modelling Cubical Type Theory in a Topos},
 editor       = {J.-M. Talbot and L.~Regnier},
 booktitle    = {25th EACSL Annual Conference on Computer Science Logic ({CSL} 2016)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {62},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f\"ur Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {24:1--24:19},
 doi          = {10.4230/LIPIcs.CSL.2016.24},
)
@misc(agdacode,
 author       = {A.~M. Pitts and S.~C. Steenkamp},
 year         = {2021},
 title        = {{Agda} code accompanying this paper},
 doi          = {10.17863/CAM.73911},
)
@article(RobertsDM:weacpw,
 author       = {D.~M. Roberts},
 year         = {2015},
 title        = {The Weak Choice Principle {WISC} may Fail in the Category of Sets},
 journal      = {Studia Logica},
 volume       = {103},
 pages        = {1005--1017},
 doi          = {10.1007/s11225-015-9603-6},
)
@unpublished(ShulmanM:surcpo,
 author       = {M.~Shulman},
 year         = {2014},
 title        = {The surreals contain the plump ordinals},
 url          = {https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/},
 note         = {Homotopy Type Theory blog},
)
@inproceedings(SprengerC:strirc,
 author       = {C.~Sprenger and M.~Dam},
 year         = {2003},
 title        = {On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the $\mu$Calculus},
 editor       = {A.~D. Gordon},
 booktitle    = {Foundations of Software Science and Computation Structures (FoSSaCS 2003)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2620},
 publisher    = {Springer, Berlin, Heidelberg.},
 pages        = {425--440},
 doi          = {10.1007/3-540-36576-1{\_}27},
)
@unpublished(StreicherT:reamc,
 author       = {T.~Streicher},
 year         = {2005},
 title        = {Realizability Models for {CZF} + $\neg$ Pow},
 url          = {http://www2.mathematik.tu-darmstadt.de/~streicher/CIZF/rmczfnp.pdf},
 note         = {Unpublished note},
)
@incollection(StreicherT:unit,
 author       = {T.~Streicher},
 year         = {2005},
 title        = {Universes in Toposes},
 editor       = {L.~Crosilla and P.~Schuster},
 booktitle    = {From Sets and Types to Topology and Analysis, Towards Practicable Foundations for Constructive Mathematics},
 chapter      = {4},
 series       = {Oxford Logic Guides},
 volume       = {48},
 publisher    = {Oxford University Press},
 pages        = {78--90},
 doi          = {10.1093/acprof:oso/9780198566519.001.0001},
)
@article(swan2018wtypes,
 author       = {A.~Swan},
 year         = {2018},
 title        = {{W}-Types with Reductions and the Small Object Argument},
 journal      = {ArXiv e-prints},
 volume       = {arXiv:1802.07588 [math.CT]},
 url          = {https://arxiv.org/abs/1802.07588},
)
@article(TaylorP:intso,
 author       = {P.~Taylor},
 year         = {1996},
 title        = {Intuitionistic Sets and Ordinals},
 journal      = {Journal of Symbolic Logic},
 volume       = {61},
 pages        = {705--744},
 doi          = {10.2307/2275781},
)
@book(TaylorP:prafm,
 author       = {P.~Taylor},
 year         = {1999},
 title        = {Practical Foundations of Mathematics},
 series       = {Cambridge Studies in Advanced Mathematics},
 volume       = {59},
 publisher    = {Cambridge University Press},
)
@book(HoTT,
 author       = {{Univalent Foundations Program}, The},
 year         = {2013},
 title        = {Homotopy Type Theory: Univalent Foundations for Mathematics},
 publisher    = {Institute for Advanced Study},
 url          = {http://homotopytypetheory.org/book},
)
@article(vandenberg2014axiom,
 author       = {B.~{van den Berg} and I.~Moerdijk},
 year         = {2014},
 title        = {The Axiom of Multiple Choice and Models for Constructive Set Theory},
 journal      = {Journal of Mathematical Logic},
 volume       = {14},
 number       = {01},
 pages        = {1450005},
 doi          = {10.1142/S0219061314500056},
)