@unpublished{coquandConstructiveSheafModels2020,
  title = {Constructive Sheaf Models of Type Theory},
  author = {Coquand, Thierry and Ruch, Fabian and Sattler, Christian},
  date = {2020-07-08},
  eprint = {1912.10407},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1912.10407},
  urldate = {2022-04-25},
  abstract = {We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.},
  keywords = {Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/BM86P38T/Coquand et al. - 2020 - Constructive sheaf models of type theory.pdf;/home/nerf/Zotero/storage/VIMEBY7W/1912.html}
}

@unpublished{gambinoEffectiveModelStructure2021,
  title = {The Effective Model Structure and \$\textbackslash infty\$-Groupoid Objects},
  author = {Gambino, Nicola and Henry, Simon and Sattler, Christian and Szumiło, Karol},
  date = {2021-03-10},
  eprint = {2102.06146},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/2102.06146},
  urldate = {2022-04-25},
  abstract = {For a category \$\textbackslash mathcal E\$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in \$\textbackslash mathcal E\$, generalising the Kan--Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated \$\textbackslash infty\$-category has finite limits, colimits satisfying descent, and is locally Cartesian closed when \$\textbackslash mathcal E\$ is, but is not a higher topos in general. We also characterise the \$\textbackslash infty\$-category presented by the effective model structure, showing that it is the full sub-category of presheaves on \$\textbackslash mathcal E\$ spanned by Kan complexes in \$\textbackslash mathcal E\$, a result that suggests a close analogy with the theory of exact completions.},
  keywords = {18N40 (primary) 18N60 55U10,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/QVGLME2U/Gambino et al. - 2021 - The effective model structure and $infty$-groupoi.pdf;/home/nerf/Zotero/storage/2YSZT8KA/2102.html}
}

@article{bergerExtensionNotionReedy2011,
  title = {On an Extension of the Notion of {{Reedy}} Category},
  author = {Berger, Clemens and Moerdijk, Ieke},
  date = {2011-12},
  journaltitle = {Mathematische Zeitschrift},
  shortjournal = {Math. Z.},
  volume = {269},
  number = {3-4},
  eprint = {0809.3341},
  eprinttype = {arXiv},
  pages = {977--1004},
  issn = {0025-5874, 1432-1823},
  doi = {10.1007/s00209-010-0770-x},
  url = {http://arxiv.org/abs/0809.3341},
  urldate = {2022-04-26},
  abstract = {We extend the classical notion of a Reedy category so as to allow non-trivial automorphisms. Our extension includes many important examples occuring in topology such as Segal's category Gamma, or the total category of a crossed simplicial group such as Connes' cyclic category Lambda. For any generalized Reedy category R and any cofibrantly generated model category E, the functor category E\textasciicircum R is shown to carry a canonical model structure of Reedy type.},
  keywords = {18G55 55U35 (Primary) 18G30 20N99 (Secondary),absolute pushouts,Eilenberg-Zilber Category,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/9CXJYQ22/Berger and Moerdijk - 2011 - On an extension of the notion of Reedy category.pdf;/home/nerf/Zotero/storage/E9DB6IW2/0809.html}
}

@article{garnerUnderstandingSmallObject2009,
  title = {Understanding the Small Object Argument},
  author = {Garner, Richard},
  date = {2009-06},
  journaltitle = {Applied Categorical Structures},
  shortjournal = {Appl Categor Struct},
  volume = {17},
  number = {3},
  eprint = {0712.0724},
  eprinttype = {arXiv},
  pages = {247--285},
  issn = {0927-2852, 1572-9095},
  doi = {10.1007/s10485-008-9137-4},
  url = {http://arxiv.org/abs/0712.0724},
  urldate = {2022-04-26},
  abstract = {The small object argument is a transfinite construction which, starting from a set of maps in a category, generates a weak factorisation system on that category. As useful as it is, the small object argument has some problematic aspects: it possesses no universal property; it does not converge; and it does not seem to be related to other transfinite constructions occurring in categorical algebra. In this paper, we give an "algebraic" refinement of the small object argument, cast in terms of Grandis and Tholen's natural weak factorisation systems, which rectifies each of these three deficiencies.},
  keywords = {18A32 55U35,18C10,55U35,Algebraic model structures,Mathematics - Algebraic Topology,Mathematics - Category Theory,Small object argument,Weak factorisation system},
  file = {/home/nerf/Zotero/storage/7UVP29D5/Garner - 2009 - Understanding the Small Object Argument.pdf;/home/nerf/Zotero/storage/9V4MZU3G/Garner - 2009 - Understanding the small object argument.pdf;/home/nerf/Zotero/storage/8TPNVUAK/0712.html}
}

@unpublished{riehlAlgebraicModelStructures2011,
  title = {Algebraic Model Structures},
  author = {Riehl, Emily},
  date = {2011-03-11},
  eprint = {0910.2733},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/0910.2733},
  urldate = {2022-04-26},
  abstract = {We define a new notion of an algebraic model structure, in which the cofibrations and fibrations are retracts of coalgebras for comonads and algebras for monads, and prove "algebraic" analogs of classical results. Using a modified version of Quillen's small object argument, we show that every cofibrantly generated model structure in the usual sense underlies a cofibrantly generated algebraic model structure. We show how to pass a cofibrantly generated algebraic model structure across an adjunction, and we characterize the algebraic Quillen adjunction that results. We prove that pointwise natural weak factorization systems on diagram categories are cofibrantly generated if the original ones are, and we give an algebraic generalization of the projective model structure. Finally, we prove that certain fundamental comparison maps present in any cofibrantly generated model category are cofibrations when the cofibrations are monomorphisms, a conclusion that does not seem to be provable in the classical, non-algebraic, theory.},
  keywords = {55U35 18A32,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/7748DLXS/Riehl - 2011 - Algebraic model structures.pdf;/home/nerf/Zotero/storage/5TLYJVHI/0910.html}
}

@article{bourkeAlgebraicWeakFactorisation2016,
  title = {Algebraic Weak Factorisation Systems {{I}}: Accessible {{AWFS}}},
  shorttitle = {Algebraic Weak Factorisation Systems {{I}}},
  author = {Bourke, John and Garner, Richard},
  date = {2016-01},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {220},
  number = {1},
  eprint = {1412.6559},
  eprinttype = {arXiv},
  pages = {108--147},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2015.06.002},
  url = {http://arxiv.org/abs/1412.6559},
  urldate = {2022-04-26},
  abstract = {Algebraic weak factorisation systems (AWFS) refine weak factorisation systems by requiring that the assignations sending a map to its first and second factors should underlie an interacting comonad--monad pair on the arrow category. We provide a comprehensive treatment of the basic theory of AWFS---drawing on work of previous authors---and complete the theory with two main new results. The first provides a characterisation of AWFS and their morphisms in terms of their double categories of left or right maps. The second concerns a notion of cofibrant generation of an AWFS by a small double category; it states that, over a locally presentable base, any small double category cofibrantly generates an AWFS, and that the AWFS so arising are precisely those with accessible monad and comonad. Besides the general theory, numerous applications of AWFS are developed, emphasising particularly those aspects which go beyond the non-algebraic situation.},
  keywords = {18A32 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/NSWFIVRX/Bourke and Garner - 2016 - Algebraic weak factorisation systems I accessible.pdf;/home/nerf/Zotero/storage/EHWCEUH2/1412.html}
}

@article{bourkeAlgebraicWeakFactorisation2016a,
  title = {Algebraic Weak Factorisation Systems {{II}}: Categories of Weak Maps},
  shorttitle = {Algebraic Weak Factorisation Systems {{II}}},
  author = {Bourke, John and Garner, Richard},
  date = {2016-01},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {220},
  number = {1},
  eprint = {1412.6560},
  eprinttype = {arXiv},
  pages = {148--174},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2015.06.003},
  url = {http://arxiv.org/abs/1412.6560},
  urldate = {2022-04-26},
  abstract = {We investigate the categories of weak maps associated to an algebraic weak factorisation system (AWFS) in the sense of Grandis-Tholen. For any AWFS on a category with an initial object, cofibrant replacement forms a comonad, and the category of (left) weak maps associated to the AWFS is by definition the Kleisli category of this comonad. We exhibit categories of weak maps as a kind of "homotopy category", that freely adjoins a section for every "acyclic fibration" (=right map) of the AWFS; and using this characterisation, we give an alternate description of categories of weak maps in terms of spans with left leg an acyclic fibration. We moreover show that the 2-functor sending each AWFS on a suitable category to its cofibrant replacement comonad has a fully faithful right adjoint: so exhibiting the theory of comonads, and dually of monads, as incorporated into the theory of AWFS. We also describe various applications of the general theory: to the generalised sketches of Kinoshita-Power-Takeyama, to the two-dimensional monad theory of Blackwell-Kelly-Power, and to the theory of dg-categories.},
  keywords = {18A32 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/PY6J3T45/Bourke and Garner - 2016 - Algebraic weak factorisation systems II categorie.pdf;/home/nerf/Zotero/storage/5R23IT8L/1412.html}
}

@unpublished{isaacsonSymmetricCubicalSets2009,
  title = {Symmetric {{Cubical Sets}}},
  author = {Isaacson, Samuel B.},
  date = {2009-10-26},
  eprint = {0910.4948},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/0910.4948},
  urldate = {2022-04-26},
  abstract = {We introduce a new cubical model for homotopy types. More precisely, we'll define a category Qs with the following features: Qs is a PROP containing the classical box category as a subcategory, the category Qs-Set of presheaves of sets on Qs models the homotopy category, and combinatorial symmetric monoidal model categories with cofibrant unit all have homotopically well behaved Qs-Set enrichments.},
  keywords = {55u35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/QGG5W5Q5/Isaacson - 2009 - Symmetric Cubical Sets.pdf;/home/nerf/Zotero/storage/ZN3NRQN4/0910.html}
}

@book{quillenHomotopicalAlgebra1967,
  title = {Homotopical {{Algebra}}},
  author = {Quillen, Daniel G.},
  editor = {Dold, A. and Eckmann, B.},
  editortype = {redactor},
  date = {1967},
  series = {Lecture {{Notes}} in {{Mathematics}}},
  volume = {43},
  publisher = {Springer},
  location = {Berlin, Heidelberg},
  doi = {10.1007/BFb0097438},
  url = {http://link.springer.com/10.1007/BFb0097438},
  urldate = {2022-04-27},
  isbn = {978-3-540-03914-3 978-3-540-35523-6},
  keywords = {algebra,homotopical algebra,Homotopie,homotopy,homotopy theory,Quillen},
  file = {/home/nerf/Zotero/storage/JG33WVEZ/Quillen - 1967 - Homotopical Algebra.pdf}
}

@article{grandisNaturalWeakFactorization2006,
  title = {Natural Weak Factorization Systems},
  author = {Grandis, Marco and Tholen, Walter},
  date = {2006-01-01},
  journaltitle = {Archivum Mathematicum},
  shortjournal = {Archivum Mathematicum},
  volume = {42},
  abstract = {In order to facilitate a natural choice for morphisms created by the (left or right) lifting property as used in the definition of weak factorization systems, the notion of natural weak factorization system in the category K is introduced, as a pair (comonad, monad) over K 2 . The link with existing notions in terms of morphism classes is given via the respective Eilenberg–Moore categories.},
  file = {/home/nerf/Zotero/storage/PKDDLPTE/Grandis and Tholen - 2006 - Natural weak factorization systems.pdf}
}

@unpublished{gambinoConstructiveKanQuillenModel2021,
  title = {The Constructive {{Kan-Quillen}} Model Structure: Two New Proofs},
  shorttitle = {The Constructive {{Kan-Quillen}} Model Structure},
  author = {Gambino, Nicola and Sattler, Christian and Szumiło, Karol},
  date = {2021-11-22},
  eprint = {1907.05394},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1907.05394},
  urldate = {2022-04-29},
  abstract = {We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.},
  keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/G66J48KN/Gambino et al. - 2021 - The constructive Kan-Quillen model structure two .pdf;/home/nerf/Zotero/storage/IQ2BSHPM/1907.html}
}

@article{gambinoFrobeniusConditionRight2017,
  title = {The {{Frobenius Condition}}, {{Right Properness}}, and {{Uniform Fibrations}}},
  author = {Gambino, Nicola and Sattler, Christian},
  date = {2017-12},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {221},
  number = {12},
  eprint = {1510.00669},
  eprinttype = {arXiv},
  pages = {3027--3068},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2017.02.013},
  url = {http://arxiv.org/abs/1510.00669},
  urldate = {2022-04-29},
  abstract = {We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.},
  keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic,Unknown Paper?},
  file = {/home/nerf/Zotero/storage/SVIAPJW5/Gambino and Sattler - 2017 - The Frobenius Condition, Right Properness, and Uni.pdf;/home/nerf/Zotero/storage/DTMPA7ZW/1510.html;/home/nerf/Zotero/storage/NLPL6A6T/1510.html}
}

@unpublished{LOPS,
  title = {Internal {{Universes}} in {{Models}} of {{Homotopy Type Theory}}},
  author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
  date = {2018},
  eprint = {1801.07664},
  eprinttype = {arXiv},
  eprintclass = {cs},
  pages = {17 pages},
  doi = {10.4230/LIPIcs.FSCD.2018.22},
  url = {http://arxiv.org/abs/1801.07664},
  urldate = {2022-05-11},
  abstract = {We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-M\textbackslash "ortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.},
  shorthand = {LOPS},
  version = {2},
  keywords = {Computer Science - Logic in Computer Science,F.3.2,F.4.1,LOPS,Tiny},
  file = {/home/nerf/Zotero/storage/58IRMAVX/Licata et al. - 2018 - Internal Universes in Models of Homotopy Type Theo.pdf;/home/nerf/Zotero/storage/9H5DEUV7/1801.html}
}

@unpublished{ortonAxiomsModellingCubical2018,
  title = {Axioms for {{Modelling Cubical Type Theory}} in a {{Topos}}},
  author = {Orton, Ian and Pitts, Andrew M.},
  date = {2018-12-08},
  eprint = {1712.04864},
  eprinttype = {arXiv},
  eprintclass = {cs},
  doi = {10.23638/LMCS-14(4:23)2018},
  url = {http://arxiv.org/abs/1712.04864},
  urldate = {2022-05-11},
  abstract = {The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object \$I\$ in a topos to give such a path-based model of type theory in which paths are just functions with domain \$I\$. Cohen, Coquand, Huber and M\textbackslash "ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)},
  keywords = {Computer Science - Logic in Computer Science,F.4.1},
  file = {/home/nerf/Zotero/storage/IPQSVWQ9/Orton and Pitts - 2018 - Axioms for Modelling Cubical Type Theory in a Topo.pdf;/home/nerf/Zotero/storage/KRK2SGUB/1712.html}
}

@article{awodeyQuillenModelStructures,
  title = {Quillen Model Structures on Cubical Sets},
  author = {Awodey, Steve},
  pages = {31},
  langid = {english},
  file = {/home/nerf/Zotero/storage/79HSXCBI/Awodey - Quillen model structures on cubical sets.pdf}
}

@video{riehlVid,
  entrysubtype = {video},
  title = {The {{Equivariant Uniform Kan Fibration Model}} of {{Cubical Homotopy Type Theory}} - {{YouTube}}},
  editor = {Riehl, Emily},
  editortype = {director},
  date = {2020-05-26},
  url = {https://www.youtube.com/watch?v=A8tEwxM7uxE},
  urldate = {2022-06-19},
  abstract = {Dr Emily Riehl  Johns Hopkins University},
  file = {/home/nerf/Zotero/storage/SYCCCLDV/watch.html}
}

@article{borceuxCauchyCompletionCategory1986,
  title = {Cauchy completion in category theory},
  author = {Borceux, Francis and Dejean, Dominique},
  date = {1986},
  journaltitle = {Cahiers de Topologie et Géométrie Différentielle Catégoriques},
  volume = {27},
  number = {2},
  pages = {133--146},
  url = {http://www.numdam.org/item/?id=CTGDC_1986__27_2_133_0},
  urldate = {2022-08-31},
  langid = {french},
  file = {/home/nerf/Zotero/storage/K5TFJMSJ/Borceux and Dejean - 1986 - Cauchy completion in category theory.pdf;/home/nerf/Zotero/storage/VQ499FFR/item.html}
}

@article{riehlTOPOSSEMANTICSHOMOTOPY,
  title = {{{ON THE}} ∞-{{TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY}}},
  author = {Riehl, Emily},
  pages = {37},
  abstract = {Many introductions to homotopy type theory and the univalence axiom neglect to explain what any of it means, glossing over the semantics of this new formal system in traditional set-based foundations. This series of talks will attempt to survey the state of the art, first presenting Voevodsky’s simplicial model of univalent foundations and then touring Shulman’s vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ∞-topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.},
  langid = {english},
  file = {/home/nerf/Zotero/storage/UA9ZRJ5Y/Riehl - ON THE ∞-TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY.pdf}
}

@online{gratzerStrictUniversesGrothendieck2022,
  title = {Strict Universes for {{Grothendieck}} Topoi},
  author = {Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan},
  date = {2022-03-15},
  eprint = {2202.12012},
  eprinttype = {arXiv},
  eprintclass = {cs, math},
  doi = {10.48550/arXiv.2202.12012},
  url = {http://arxiv.org/abs/2202.12012},
  urldate = {2022-08-31},
  abstract = {Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-L\textbackslash "of type theory. We observe that a slight adjustment to an argument of Shulman constructs a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct-style interpretations of Martin-L\textbackslash "of type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi.},
  pubstate = {prepublished},
  keywords = {Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/IREIT5EI/Gratzer et al. - 2022 - Strict universes for Grothendieck topoi.pdf;/home/nerf/Zotero/storage/QZ4LQ95R/2202.html}
}

@online{cavalloRelativeEleganceCartesian2022,
  title = {Relative Elegance and Cartesian Cubes with One Connection},
  author = {Cavallo, Evan and Sattler, Christian},
  date = {2022-11-27},
  eprint = {2211.14801},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.2211.14801},
  url = {http://arxiv.org/abs/2211.14801},
  urldate = {2022-12-16},
  abstract = {We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a model of a cubical type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first known example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.},
  pubstate = {prepublished},
  keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/GH8VCM2Q/Cavallo and Sattler - 2022 - Relative elegance and cartesian cubes with one con.pdf;/home/nerf/Zotero/storage/75FUEPL2/2211.html}
}

@online{castellanCategoriesFamiliesUnityped2020a,
  title = {Categories with {{Families}}: {{Unityped}}, {{Simply Typed}}, and {{Dependently Typed}}},
  shorttitle = {Categories with {{Families}}},
  author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter},
  date = {2020-07-07},
  eprint = {1904.00827},
  eprinttype = {arXiv},
  eprintclass = {cs},
  doi = {10.48550/arXiv.1904.00827},
  url = {http://arxiv.org/abs/1904.00827},
  urldate = {2023-03-11},
  abstract = {We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.},
  pubstate = {prepublished},
  keywords = {Computer Science - Logic in Computer Science},
  file = {/home/nerf/Zotero/storage/D6MP7U8C/Castellan et al. - 2020 - Categories with Families Unityped, Simply Typed, .pdf;/home/nerf/Zotero/storage/9E9C3MVL/1904.html}
}

@article{ABCHFL,
  title = {Syntax and Models of {{Cartesian}} Cubical Type Theory},
  author = {Angiuli, Carlo and Brunerie, Guillaume and Coquand, Thierry and Harper, Robert and Hou (Favonia), Kuen-Bang and Licata, Daniel R.},
  date = {2021-04},
  journaltitle = {Mathematical Structures in Computer Science},
  volume = {31},
  number = {4},
  pages = {424--468},
  publisher = {Cambridge University Press},
  issn = {0960-1295, 1469-8072},
  doi = {10.1017/S0960129521000347},
  url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/syntax-and-models-of-cartesian-cubical-type-theory/01B9E98DF997F0861E4BA13A34B72A7D},
  urldate = {2023-04-21},
  abstract = {We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.},
  langid = {english},
  keywords = {ABCHFL,cubical type theory,homotopy type theory,Type theory},
  file = {/home/nerf/Zotero/storage/2MPEKIEC/Angiuli et al. - 2021 - Syntax and models of Cartesian cubical type theory.pdf}
}

@article{hofmannDoctorPhilosophyUniversity,
  title = {Doctor of {{Philosophy University}} of {{Edinburgh}} 1995},
  author = {Hofmann, Martin},
  langid = {english},
  file = {/home/nerf/Zotero/storage/VKM9TK2D/Hofmann - Doctor of Philosophy University of Edinburgh 1995.pdf}
}

@book{jacobsCategoricalLogicType1999,
  title = {Categorical Logic and Type Theory},
  author = {Jacobs, Bart},
  date = {1999},
  series = {Studies in Logic and the Foundations of Mathematics},
  edition = {1st ed},
  number = {v. 141},
  publisher = {Elsevier Science},
  location = {Amsterdam ; New York},
  isbn = {978-0-444-50170-7},
  langid = {english},
  pagetotal = {760},
  keywords = {Categories (Mathematics),Type theory},
  file = {/home/nerf/Zotero/storage/BKE5ASHQ/Jacobs - 1999 - Categorical logic and type theory.pdf}
}

@book{riehlCategoricalHomotopyTheory2014,
  title = {Categorical {{Homotopy Theory}}},
  author = {Riehl, Emily},
  date = {2014},
  series = {New {{Mathematical Monographs}}},
  publisher = {Cambridge University Press},
  location = {Cambridge},
  doi = {10.1017/CBO9781107261457},
  url = {https://www.cambridge.org/core/books/categorical-homotopy-theory/556C7A200B521E61466BB7763C49DDA4},
  urldate = {2023-07-07},
  abstract = {This book develops abstract homotopy theory from the categorical perspective with a particular focus on examples. Part I discusses two competing perspectives by which one typically first encounters homotopy (co)limits: either as derived functors definable when the appropriate diagram categories admit a compatible model structure, or through particular formulae that give the right notion in certain examples. Emily Riehl unifies these seemingly rival perspectives and demonstrates that model structures on diagram categories are irrelevant. Homotopy (co)limits are explained to be a special case of weighted (co)limits, a foundational topic in enriched category theory. In Part II, Riehl further examines this topic, separating categorical arguments from homotopical ones. Part III treats the most ubiquitous axiomatic framework for homotopy theory - Quillen's model categories. Here, Riehl simplifies familiar model categorical lemmas and definitions by focusing on weak factorization systems. Part IV introduces quasi-categories and homotopy coherence.},
  isbn = {978-1-107-04845-4},
  file = {/home/nerf/Zotero/storage/NEXTFSKD/Riehl - Categorical homotopy theory.pdf;/home/nerf/Zotero/storage/IJYSYMC6/556C7A200B521E61466BB7763C49DDA4.html}
}

@online{sattlerIdempotentCompletionCubes2019,
  title = {Idempotent Completion of Cubes in Posets},
  author = {Sattler, Christian},
  date = {2019-03-08},
  eprint = {1805.04126},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.1805.04126},
  url = {http://arxiv.org/abs/1805.04126},
  urldate = {2023-08-23},
  abstract = {This note concerns the category \$\textbackslash Box\$ of cartesian cubes with connections, equivalently the full subcategory of posets on objects \$[1]\textasciicircum n\$ with \$n \textbackslash geq 0\$. We show that the idempotent completion of \$\textbackslash Box\$ consists of finite complete posets. It follows that cubical sets, ie presheaves over \$\textbackslash Box\$, are equivalent to presheaves over finite complete posets. This yields an alternative exposition of a result by Kapulkin and Voevodsky that simplicial sets form a subtopos of cubical sets.},
  pubstate = {prepublished},
  keywords = {Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/SYH7C9JV/Sattler - 2019 - Idempotent completion of cubes in posets.pdf;/home/nerf/Zotero/storage/9ZN8RBCZ/1805.html}
}

@online{sattlerEquivalenceExtensionProperty2017,
  title = {The {{Equivalence Extension Property}} and {{Model Structures}}},
  author = {Sattler, Christian},
  date = {2017-04-23},
  url = {https://arxiv.org/abs/1704.06911v4},
  urldate = {2023-08-23},
  abstract = {We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex\textasciicircum infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.},
  langid = {english},
  pubstate = {prepublished},
  keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic,The unknown Paper?},
  file = {/home/nerf/Zotero/storage/GFLT3HLU/Sattler - 2017 - The Equivalence Extension Property and Model Struc.pdf;/home/nerf/Zotero/storage/FDPHZXNP/1704.html;/home/nerf/Zotero/storage/SEADD4R7/1704.html}
}

@online{dohertyCubicalModelsInfty2020,
  title = {Cubical Models of \$(\textbackslash infty, 1)\$-Categories},
  author = {Doherty, Brandon and Kapulkin, Chris and Lindsey, Zachery and Sattler, Christian},
  date = {2020-05-11},
  url = {https://arxiv.org/abs/2005.04853v3},
  urldate = {2023-08-23},
  abstract = {We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We show that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. As an application, we show that cubical quasicategories admit a convenient notion of a mapping space, which we use to characterize the weak equivalences between fibrant objects in our model structure as DK-equivalences.},
  langid = {english},
  organization = {arXiv.org},
  file = {/home/nerf/Zotero/storage/6F6WV5U3/Doherty et al. - 2020 - Cubical models of $(infty, 1)$-categories.pdf}
}

@inproceedings{cavalloUnifyingCubicalModels2020,
  title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}},
  booktitle = {28th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2020)},
  author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W.},
  editor = {Fernández, Maribel and Muscholl, Anca},
  date = {2020},
  series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})},
  volume = {152},
  pages = {14:1--14:17},
  publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik},
  location = {Dagstuhl, Germany},
  issn = {1868-8969},
  doi = {10.4230/LIPIcs.CSL.2020.14},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/11657},
  urldate = {2023-08-23},
  isbn = {978-3-95977-132-0},
  keywords = {Cubical Set Models,Cubical Type Theory,examples composition structures,Homotopy Type Theory,Univalent Foundations},
  file = {/home/nerf/Zotero/storage/HMQ4GBI5/Cavallo et al. - 2020 - Unifying Cubical Models of Univalent Type Theory.pdf;/home/nerf/Zotero/storage/K2D9KNGG/11657.html}
}

@inproceedings{bezemModelTypeTheory2014,
  title = {A {{Model}} of {{Type Theory}} in {{Cubical Sets}}},
  author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  namea = {Herbstritt, Marc},
  nameatype = {collaborator},
  date = {2014},
  pages = {22 pages},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany},
  doi = {10.4230/LIPICS.TYPES.2013.107},
  url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628/},
  urldate = {2023-08-28},
  abstract = {We present a model of type theory with dependent product, sum, and  identity, in cubical sets. We describe a universe and explain how  to transform an equivalence between two types into an equality. We  also explain how to model propositional truncation and the circle.  While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.},
  langid = {english},
  keywords = {000 Computer science knowledge general works,Computer Science},
  file = {/home/nerf/Zotero/storage/4KKXST7S/Bezem et al. - A model of type theory in cubical sets.pdf}
}

@inproceedings{dybjerInternalTypeTheory2003,
  title = {Internal {{Type Theory}}},
  author = {Dybjer, Peter},
  date = {2003-06-23},
  doi = {10.1007/3-540-61780-9_66},
  abstract = {We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to ordinary syntax and yet has a clean categorical description. We also present categories with families as a generalized algebraic theory. Then we define categories with families formally in Martin-Lof's intensional intuitionistic type theory. Finally, we discuss the coherence problem for these internal categories with families.},
  isbn = {978-3-540-61780-8},
  keywords = {CwF,Families},
  file = {/home/nerf/Zotero/storage/MKQRDD7X/Dybjer - 2003 - Internal Type Theory.pdf}
}

@book{streicherSemanticsTypeTheory1991,
  title = {Semantics of {{Type Theory}}},
  author = {Streicher, Thomas},
  date = {1991},
  publisher = {Birkhäuser Boston},
  location = {Boston, MA},
  doi = {10.1007/978-1-4612-0433-6},
  url = {http://link.springer.com/10.1007/978-1-4612-0433-6},
  urldate = {2023-09-02},
  isbn = {978-1-4612-6757-7 978-1-4612-0433-6},
  langid = {english},
  file = {/home/nerf/Zotero/storage/ALA3AMGY/Streicher - 1991 - Semantics of Type Theory.pdf}
}

@article{hofmannSyntaxSemanticsDependent,
  title = {Syntax and {{Semantics}} of {{Dependent Types}}},
  author = {Hofmann, Martin},
  langid = {english},
  keywords = {CwF,Families,Presheaf model},
  file = {/home/nerf/Zotero/storage/NY2W23FP/Hofmann - Syntax and Semantics of Dependent Types.pdf}
}

@book{maclaneCategoriesWorkingMathematician1978,
  title = {Categories for the {{Working Mathematician}}},
  author = {Mac Lane, Saunders},
  date = {1978},
  series = {Graduate {{Texts}} in {{Mathematics}}},
  volume = {5},
  publisher = {Springer},
  location = {New York, NY},
  doi = {10.1007/978-1-4757-4721-8},
  url = {http://link.springer.com/10.1007/978-1-4757-4721-8},
  urldate = {2023-09-12},
  isbn = {978-1-4419-3123-8 978-1-4757-4721-8},
  keywords = {addition,Adjoint functor,algebra,Morphism,theorem},
  file = {/home/nerf/Zotero/storage/LCQ4M4Q8/Mac Lane - 1978 - Categories for the Working Mathematician.pdf}
}

@book{awodeyCategoryTheory2006,
  title = {Category {{Theory}}},
  author = {Awodey, Steve},
  date = {2006-05-25},
  publisher = {Oxford University Press},
  doi = {10.1093/acprof:oso/9780198568612.001.0001},
  url = {https://doi.org/10.1093/acprof:oso/9780198568612.001.0001},
  urldate = {2023-09-12},
  abstract = {This book is a text and reference book on Category Theory, a branch of abstract algebra. The book contains clear definitions of the essential concepts, which are illuminated with numerous accessible examples. It provides full proofs of all the important propositions and theorems, and aims to make the basic ideas, theorems, and methods of Category Theory understandable. Although it assumes few mathematical pre-requisites, the standard of mathematical rigour is not compromised. The material covered includes the standard core of categories; functors; natural transformations; equivalence; limits and colimits; functor categories; representables; Yoneda's lemma; adjoints; and monads. An extra topic of cartesian closed categories and the lambda-calculus is also provided.},
  isbn = {978-0-19-856861-2}
}

@book{maclaneSheavesGeometryLogic1994,
  title = {Sheaves in {{Geometry}} and {{Logic}}: {{A First Introduction}} to {{Topos Theory}}},
  shorttitle = {Sheaves in {{Geometry}} and {{Logic}}},
  author = {Mac Lane, Saunders and Moerdijk, Ieke},
  date = {1994},
  series = {Universitext},
  publisher = {Springer},
  location = {New York, NY},
  doi = {10.1007/978-1-4612-0927-0},
  url = {https://link.springer.com/10.1007/978-1-4612-0927-0},
  urldate = {2023-09-12},
  isbn = {978-0-387-97710-2 978-1-4612-0927-0},
  langid = {english},
  keywords = {Algebraic structure,Boolean algebra,Division,forcing,Heyting algebra,set,set theory},
  file = {/home/nerf/Zotero/storage/W58HYMXM/Mac Lane and Moerdijk - 1994 - Sheaves in Geometry and Logic A First Introductio.pdf}
}

@online{IntroductionHomotopyTheory,
  title = {Introduction to {{Homotopy Theory}} in {{nLab}}},
  url = {https://ncatlab.org/nlab/show/Introduction+to+Homotopy+Theory},
  urldate = {2023-09-12},
  file = {/home/nerf/Zotero/storage/77QL5DY8/Introduction+to+Homotopy+Theory.html}
}

@book{hirschhornModelCategoriesTheir2009,
  title = {Model {{Categories}} and {{Their Localizations}}},
  author = {Hirschhorn, Philip},
  date = {2009-08-24},
  series = {Mathematical {{Surveys}} and {{Monographs}}},
  volume = {99},
  publisher = {American Mathematical Society},
  issn = {0076-5376, 2331-7159},
  doi = {10.1090/surv/099},
  url = {https://www.ams.org/surv/099},
  urldate = {2023-09-12},
  abstract = {Advancing research. Creating connections.},
  isbn = {978-0-8218-4917-0 978-1-4704-1326-2},
  langid = {english}
}

@article{cavalloUnifyingCubicalModels2016,
  title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}},
  author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W},
  date = {2016},
  langid = {english},
  file = {/home/nerf/Zotero/storage/UDTLUHWA/Cavallo et al. - 2016 - Unifying Cubical Models of Univalent Type Theory.pdf}
}

@inbook{lawvereAlgebraicProblemsContext1968,
  title = {Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories},
  booktitle = {Reports of the {{Midwest Category Seminar II}}},
  author = {Lawvere, F. William},
  editor = {MacLane, S.},
  date = {1968},
  volume = {61},
  pages = {41--61},
  publisher = {Springer Berlin Heidelberg},
  location = {Berlin, Heidelberg},
  doi = {10.1007/BFb0077116},
  url = {http://link.springer.com/10.1007/BFb0077116},
  urldate = {2023-11-13},
  bookauthor = {André, M. and Buchsbaum, D. A. and Dubuc, E. and Knighten, R. L. and Lawvere, F. W.},
  isbn = {978-3-540-04231-0 978-3-540-35863-3},
  langid = {english},
  file = {/home/nerf/Zotero/storage/QMR75KQ6/Lawvere - 1968 - Some algebraic problems in the context of functori.pdf}
}

@article{lawvereFUNCTORIALSEMANTICSALGEBRAIC1963,
  title = {{{FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES}}},
  author = {Lawvere, F. William},
  date = {1963-11},
  journaltitle = {Proceedings of the National Academy of Sciences},
  shortjournal = {Proc. Natl. Acad. Sci. U.S.A.},
  volume = {50},
  number = {5},
  pages = {869--872},
  issn = {0027-8424, 1091-6490},
  doi = {10.1073/pnas.50.5.869},
  url = {https://pnas.org/doi/full/10.1073/pnas.50.5.869},
  urldate = {2023-11-13},
  langid = {english},
  file = {/home/nerf/Zotero/storage/ECTRWE4B/Lawvere - 1963 - FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES.pdf}
}

@incollection{streicherUNIVERSESTOPOSES2005,
  title = {{{UNIVERSES IN TOPOSES}}},
  booktitle = {From {{Sets}} and {{Types}} to {{Topology}} and {{Analysis}}},
  author = {Streicher, Thomas},
  editor = {Crosilla, Laura and Schuster, Peter},
  date = {2005-10-06},
  edition = {1},
  pages = {78--90},
  publisher = {Oxford University PressOxford},
  doi = {10.1093/acprof:oso/9780198566519.003.0005},
  url = {https://academic.oup.com/book/5354/chapter/148144921},
  urldate = {2023-11-14},
  abstract = {We discuss a notion of universe in toposes which from a logical point of view gives rise to an extension of Higher Order Intuitionistic Arithmetic (HAH) that allows one to construct families of types in such a universe by structural recursion and to quantify over such families. Further, we show that (hierarchies of) such universes do exist in all sheaf and realizability toposes but neither in the free topos nor in the Vω+ω model of Zermelo set theory.},
  isbn = {978-0-19-856651-9 978-0-19-171392-7},
  langid = {english},
  file = {/home/nerf/Zotero/storage/CB5TH6EV/Streicher - 2005 - UNIVERSES IN TOPOSES.pdf}
}

@online{awodeyKripkeJoyalForcingType2021,
  title = {Kripke-{{Joyal}} Forcing for Type Theory and Uniform Fibrations},
  author = {Awodey, S. and Gambino, N. and Hazratpour, S.},
  date = {2021-10-27},
  eprint = {2110.14576},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.2110.14576},
  url = {http://arxiv.org/abs/2110.14576},
  urldate = {2024-02-21},
  abstract = {We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.},
  pubstate = {prepublished},
  keywords = {03G30 03B38 18F20 18N45,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/NNQITW4X/Awodey et al. - 2021 - Kripke-Joyal forcing for type theory and uniform f.pdf;/home/nerf/Zotero/storage/M3MTFM97/2110.html}
}

@online{swanDefinableNondefinableNotions2022,
  title = {Definable and {{Non-definable Notions}} of {{Structure}}},
  author = {Swan, Andrew W.},
  date = {2022-06-27},
  eprint = {2206.13643},
  eprinttype = {arXiv},
  eprintclass = {cs, math},
  doi = {10.48550/arXiv.2206.13643},
  url = {http://arxiv.org/abs/2206.13643},
  urldate = {2024-03-11},
  abstract = {Definability is a key notion in the theory of Grothendieck fibrations that characterises when an external property of objects can be accessed from within the internal logic of the base of a fibration. In this paper we consider a generalisation of definability from properties of objects to structures on objects, introduced by Shulman under the name local representability. We first develop some general theory and show how to recover existing notions due to B\textbackslash '\{e\}nabou and Johnstone as special cases. We give several examples of definable and non definable notions o structure, focusing on algebraic weak factorisation systems, which can be naturally viewed as notions of structure on codomain fibrations. Regarding definability, we give a sufficient criterion for cofibrantly generated awfs's to be definable, generalising a construction of the universe for cubical sets, but also including some very different looking examples that do not satisfy tininess in the internal sense, that exponential functors have a right adjoint. Our examples of non definability include the identification of logical principles holding for the interval objects in simplicial sets and Bezem-Coquand-Huber cubical sets that suffice to show a certain definition of Kan fibration is not definable.},
  pubstate = {prepublished},
  keywords = {03G30 18N40,Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/CJRDB5DU/Swan - 2022 - Definable and Non-definable Notions of Structure.pdf;/home/nerf/Zotero/storage/DS7C3TKZ/2206.html}
}

@online{rileyTypeTheoryTiny2024,
  title = {A {{Type Theory}} with a {{Tiny Object}}},
  author = {Riley, Mitchell},
  date = {2024-03-04},
  eprint = {2403.01939},
  eprinttype = {arXiv},
  eprintclass = {cs, math},
  doi = {10.48550/arXiv.2403.01939},
  url = {http://arxiv.org/abs/2403.01939},
  urldate = {2024-03-12},
  abstract = {We present an extension of Martin-L\textbackslash "of Type Theory that contains a tiny object; a type for which there is a right adjoint to the formation of function types as well as the expected left adjoint. We demonstrate the practicality of this type theory by proving various properties related to tininess internally and suggest a few potential applications.},
  pubstate = {prepublished},
  keywords = {Computer Science - Programming Languages,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/DM45P9J4/Riley - 2024 - A Type Theory with a Tiny Object.pdf;/home/nerf/Zotero/storage/8KAP7SMU/2403.html}
}

@article{riehlCategoryTheoryContext,
  title = {Category Theory in Context},
  author = {Riehl, Emily},
  langid = {english},
  file = {/home/nerf/Zotero/storage/4WNNYCP7/Riehl - Category theory in context.pdf}
}

@online{CCHM,
  title = {Cubical {{Type Theory}}: A Constructive Interpretation of the Univalence Axiom},
  shorttitle = {Cubical {{Type Theory}}},
  author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
  date = {2016-11-07},
  eprint = {1611.02108},
  eprinttype = {arXiv},
  eprintclass = {cs, math},
  doi = {10.48550/arXiv.1611.02108},
  url = {http://arxiv.org/abs/1611.02108},
  urldate = {2024-03-29},
  abstract = {This paper presents a type theory in which it is possible to directly manipulate \$n\$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.},
  pubstate = {prepublished},
  shorthand = {CCHM},
  keywords = {CCHM,Computer Science - Logic in Computer Science,de Morgan,F.3.2,F.4.1,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/IPGDN2AH/Cohen et al. - 2016 - Cubical Type Theory a constructive interpretation.pdf;/home/nerf/Zotero/storage/3Q8F527E/1611.html}
}

@online{riehlTheoryPracticeReedy2014,
  title = {The Theory and Practice of {{Reedy}} Categories},
  author = {Riehl, Emily and Verity, Dominic},
  date = {2014-06-03},
  eprint = {1304.6871},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.1304.6871},
  url = {http://arxiv.org/abs/1304.6871},
  urldate = {2024-04-07},
  abstract = {The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic arguments, we present streamlined proofs of a number of useful technical results, which are well known to folklore but difficult to find in the literature. While the results presented here are not new, our approach to their proofs is somewhat novel. Specifically, we reduce the much of the hard work involved to simpler computations involving weighted colimits and Leibniz (pushout-product) constructions. The general theory is developed in parallel with examples, which we use to prove that familiar formulae for homotopy limits and colimits indeed have the desired properties.},
  pubstate = {prepublished},
  keywords = {55U35 18G30 18D10,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/ME8UH6X7/Riehl and Verity - 2014 - The theory and practice of Reedy categories.pdf;/home/nerf/Zotero/storage/TU3Y2293/1304.html}
}

@article{shulmanREEDYCATEGORIESTHEIR,
  title = {{{REEDY CATEGORIES AND THEIR GENERALIZATIONS}}},
  author = {Shulman, Michael},
  abstract = {We observe that the Reedy model structure on a diagram category can be constructed by iterating an operation of “bigluing” model structures along a pair of functors and a natural transformation. This yields a new explanation of the definition of Reedy categories: they are almost exactly those small categories for which the category of diagrams and its model structure can be constructed by iterated bigluing. It also gives a consistent way to produce generalizations of Reedy categories, including the generalized Reedy categories of Cisinski and Berger–Moerdijk and the enriched Reedy categories of Angeltveit, but also new versions such as a combined notion of “enriched generalized Reedy category”.},
  langid = {english},
  file = {/home/nerf/Zotero/storage/BMRJ6NMU/Shulman - REEDY CATEGORIES AND THEIR GENERALIZATIONS.pdf}
}

@incollection{balchinBisimplicialSets2021,
  title = {Bisimplicial {{Sets}}},
  booktitle = {A {{Handbook}} of {{Model Categories}}},
  author = {Balchin, Scott},
  editor = {Balchin, Scott},
  date = {2021},
  pages = {205--215},
  publisher = {Springer International Publishing},
  location = {Cham},
  doi = {10.1007/978-3-030-75035-0_12},
  url = {https://doi.org/10.1007/978-3-030-75035-0_12},
  urldate = {2024-04-10},
  abstract = {The category of bisimplicial sets is the functor category \$\$\textbackslash mathbf\{Set\} \textasciicircum\{(\textbackslash varDelta \textasciicircum\{op\} \textbackslash times \textbackslash varDelta \textasciicircum\{op\})\}\$\$Set(Δop×Δop), which we denote \$\$\textbackslash mathbf\{ssSet\} \$\$ssSet. Equivalently, \$\$\textbackslash mathbf\{ssSet\} \$\$ssSetis the category of simplicial objects in simplicial sets, i.e., \$\$\textbackslash mathbf\{ssSet\} \textbackslash cong \textbackslash mathbf\{sSet\} \textasciicircum\{\textbackslash varDelta \textasciicircum\{op\}\}\$\$ssSet≅sSetΔop. Under this identification, one could equally call a bisimplicial set a simplicial space.},
  isbn = {978-3-030-75035-0},
  langid = {english},
  file = {/home/nerf/Zotero/storage/3LJ3IU2J/Balchin - 2021 - Bisimplicial Sets.pdf}
}

@online{NCategoryCafe,
  title = {The N-{{Category Café}}},
  url = {https://golem.ph.utexas.edu/category/2015/06/what_is_a_reedy_category.html},
  urldate = {2024-04-10},
  langid = {english},
  file = {/home/nerf/Zotero/storage/FG4SPDSM/what_is_a_reedy_category.html}
}

@incollection{riehlMadetoOrderWeakFactorization2015a,
  title = {Made-to-{{Order Weak Factorization Systems}}},
  booktitle = {Extended {{Abstracts Fall}} 2013},
  author = {Riehl, Emily},
  editor = {González, Maria Del Mar and Yang, Paul C. and Gambino, Nicola and Kock, Joachim},
  date = {2015},
  pages = {87--92},
  publisher = {Springer International Publishing},
  location = {Cham},
  doi = {10.1007/978-3-319-21284-5_17},
  url = {https://link.springer.com/10.1007/978-3-319-21284-5_17},
  urldate = {2024-04-15},
  isbn = {978-3-319-21283-8 978-3-319-21284-5},
  langid = {english},
  file = {/home/nerf/Zotero/storage/PN8KT9LC/Riehl - 2015 - Made-to-Order Weak Factorization Systems.pdf}
}

@article{riehlINDUCTIVEPRESENTATIONSGENERALIZED,
  title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}},
  author = {Riehl, Emily},
  abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.},
  langid = {english},
  file = {/home/nerf/Zotero/storage/2CCAMCEM/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf}
}

@inproceedings{angiuliCartesianCubicalComputational2018,
  title = {Cartesian {{Cubical Computational Type Theory}}: {{Constructive Reasoning}} with {{Paths}} and {{Equalities}}},
  shorttitle = {Cartesian {{Cubical Computational Type Theory}}},
  booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{CSL}}.2018.6},
  author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert},
  date = {2018},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  doi = {10.4230/LIPIcs.CSL.2018.6},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6},
  urldate = {2024-04-28},
  abstract = {We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.},
  eventtitle = {27th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2018)},
  langid = {english},
  file = {/home/nerf/Zotero/storage/XTZNK2WW/Angiuli et al. - 2018 - Cartesian Cubical Computational Type Theory Const.pdf}
}

@article{bartonModel2CategoryEnriched2019,
  title = {A {{Model}} 2-{{Category}} of {{Enriched Combinatorial Premodel Categories}}},
  author = {Barton, Reid William},
  date = {2019-09-10},
  issn = {4201-3127},
  url = {https://dash.harvard.edu/handle/1/42013127},
  urldate = {2024-04-28},
  abstract = {Quillen equivalences induce equivalences of homotopy theories and therefore form a natural choice for the "weak equivalences" between model categories. In [21], Hovey asked whether the 2-category Mod of model categories has a "model 2-category structure" with these weak equivalences. We give an example showing that Mod does not have pullbacks, so cannot be a model 2-category. We can try to repair this lack of limits by generalizing the notion of model category. The lack of limits in Mod is due to the two-out-of-three axiom, so we define a premodel category to be a complete and cocomplete category equipped with two nested weak factorization systems. Combinatorial premodel categories form a 2-category CPM with excellent algebraic properties: CPM has all limits and colimits and is equipped with a tensor product (representing Quillen bifunctors) which is adjoint to an internal Hom. The homotopy theory of a model category depends in an essential way on the weak equivalences, so it does not extend directly to premodel categories. We build a substitute homotopy theory under an additional axiom on the premodel category, which holds automatically for a premodel category enriched in a monoidal model category V. The 2-category of combinatorial V-premodel categories VCPM is simply the 2-category of modules over the monoid object V, so VCPM inherits the algebraic structure of CPM. We construct a model 2-category structure on VCPM for V a tractable symmetric monoidal model category, by adapting Szumiło's construction of a fibration category of cofibration categories [35]. For set-theoretic reasons, constructing factorizations for this model 2-category structure requires a technical variant of the small object argument which relies on an analysis of the rank of combinatoriality of a premodel category.},
  langid = {english},
  annotation = {Accepted: 2019-12-11T10:06:35Z},
  file = {/home/nerf/Zotero/storage/ALJR3L7T/Barton - 2019 - A Model 2-Category of Enriched Combinatorial Premo.pdf}
}

@online{hoveyModelCategories2007,
  title = {Model {{Categories}}},
  author = {Hovey, Mark},
  date = {2007-10-17},
  series = {Mathematical {{Surveys}} and {{Monographs}}},
  volume = {63},
  publisher = {American Mathematical Society},
  issn = {0076-5376, 2331-7159},
  doi = {10.1090/surv/063},
  url = {https://www.ams.org/surv/063},
  urldate = {2024-04-28},
  abstract = {Advancing research. Creating connections.},
  isbn = {9780821843611 9781470412906},
  langid = {english},
  organization = {American Mathematical Society}
}

@online{coquandVariationCubicalSets2014,
  title = {Variation on {{Cubical Sets}}},
  author = {Coquand, Thierry},
  date = {2014},
  url = {https://www.cse.chalmers.se/~coquand/diag.pdf},
  urldate = {2024-04-30},
  file = {/home/nerf/Zotero/storage/HQBY2TZY/diag.pdf}
}

@article{streicherSimplicialSetsCubical2021,
  title = {Simplicial Sets inside Cubical Sets},
  author = {Streicher, Thomas and Weinberger, Jonathan},
  date = {2021-03-15},
  journaltitle = {Theory and Applications of Categories},
  volume = {37},
  number = {10},
  pages = {276--286},
  url = {http://www.tac.mta.ca/tac/volumes/37/10/37-10abs.html},
  urldate = {2024-05-02},
  file = {/home/nerf/Zotero/storage/DSG2FX6B/Streicher and Weinberger - 2021 - Simplicial sets inside cubical sets.pdf}
}

@online{riehlTypeTheorySynthetic2023,
  title = {A Type Theory for Synthetic \$\textbackslash infty\$-Categories},
  author = {Riehl, Emily and Shulman, Michael},
  date = {2023-06-08},
  eprint = {1705.07442},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.1705.07442},
  url = {http://arxiv.org/abs/1705.07442},
  urldate = {2024-05-30},
  abstract = {We propose foundations for a synthetic theory of \$(\textbackslash infty,1)\$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a "dependent Yoneda lemma" that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using "extension types" that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.},
  pubstate = {prepublished},
  keywords = {03G30 18G55 55U40,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/6MQM9TWA/Riehl and Shulman - 2023 - A type theory for synthetic $infty$-categories.pdf;/home/nerf/Zotero/storage/H3UW42V3/1705.html}
}

@online{solution,
  title = {The Equivariant Model Structure on Cartesian Cubical Sets},
  author = {Awodey, Steve and Cavallo, Evan and Coquand, Thierry and Riehl, Emily and Sattler, Christian},
  date = {2024-06-26},
  eprint = {2406.18497},
  eprinttype = {arXiv},
  eprintclass = {cs, math},
  doi = {10.48550/arXiv.2406.18497},
  url = {http://arxiv.org/abs/2406.18497},
  urldate = {2024-07-03},
  abstract = {We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.},
  pubstate = {prepublished},
  shorthand = {ACCRS},
  keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/AKJBUSV6/Awodey et al. - 2024 - The equivariant model structure on cartesian cubic.pdf;/home/nerf/Zotero/storage/ZD7WA4UC/2406.html}
}

@online{awodeyHofmannStreicherUniverses2023,
  title = {On {{Hofmann-Streicher}} Universes},
  author = {Awodey, Steve},
  date = {2023-07-11},
  eprint = {2205.10917},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.2205.10917},
  url = {http://arxiv.org/abs/2205.10917},
  urldate = {2024-07-05},
  abstract = {We have another look at the construction by Hofmann and Streicher of a universe \$(U,\{\textbackslash mathsf\{E\}l\})\$ for the interpretation of Martin-L\textbackslash "of type theory in a presheaf category \$\textbackslash psh\{\textbackslash C\}\$. It turns out that \$(U,\{\textbackslash mathsf\{E\}l\})\$ can be described as the \textbackslash emph\{categorical nerve\} of the classifier \$\textbackslash dot\{\textbackslash Set\}\textasciicircum\{\textbackslash mathsf\{op\}\} \textbackslash to \textbackslash op\{\textbackslash Set\}\$ for discrete fibrations in \$\textbackslash Cat\$, where the nerve functor is right adjoint to the so-called ``Grothendieck construction'' taking a presheaf \$P : \textbackslash op\{\textbackslash C\}\textbackslash to\textbackslash Set\$ to its category of elements \$\textbackslash int\_\textbackslash C P\$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.},
  pubstate = {prepublished},
  keywords = {Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/NIIL8ZAK/Awodey - 2023 - On Hofmann-Streicher universes.pdf;/home/nerf/Zotero/storage/J3DQ66DM/2205.html}
}

@article{pareAbsoluteColimits1971,
  title = {On Absolute Colimits},
  author = {Paré, Robert},
  date = {1971-09-01},
  journaltitle = {Journal of Algebra},
  shortjournal = {Journal of Algebra},
  volume = {19},
  number = {1},
  pages = {80--95},
  issn = {0021-8693},
  doi = {10.1016/0021-8693(71)90116-5},
  url = {https://www.sciencedirect.com/science/article/pii/0021869371901165},
  urldate = {2024-07-10},
  file = {/home/nerf/Zotero/storage/E68DYK76/0021869371901165.html}
}

@online{Section00VCFunctoriality,
  title = {Section 7.5 ({{00VC}}): {{Functoriality}} of Categories of Presheaves—{{The Stacks}} Project},
  url = {https://stacks.math.columbia.edu/tag/00VC},
  urldate = {2024-07-12},
  file = {/home/nerf/Zotero/storage/LEP4E2FJ/00VC.html}
}

@inreference{stacks00VC,
  title = {The {{Stacks}} Project},
  author = {The \{Stacks project authors\}},
  url = {https://stacks.math.columbia.edu/tag/00VC}
}

@article{sattlerCYLINDRICALMODELSTRUCTURES,
  title = {{{CYLINDRICAL MODEL STRUCTURES}}},
  author = {Sattler, Christian},
  url = {https://www.cse.chalmers.se/~sattler/docs/interval-model-structure.pdf},
  langid = {english},
  file = {/home/nerf/Zotero/storage/G9NTWNAY/Sattler - CYLINDRICAL MODEL STRUCTURES.pdf}
}

@online{shulmanAllInftyToposes2019,
  title = {All \$(\textbackslash infty,1)\$-Toposes Have Strict Univalent Universes},
  author = {Shulman, Michael},
  date = {2019-04-26},
  eprint = {1904.07004},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.1904.07004},
  url = {http://arxiv.org/abs/1904.07004},
  urldate = {2024-07-23},
  abstract = {We prove the conjecture that any Grothendieck \$(\textbackslash infty,1)\$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to \$(\textbackslash infty,1)\$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.},
  pubstate = {prepublished},
  keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/STEZIS8H/Shulman - 2019 - All $(infty,1)$-toposes have strict univalent uni.pdf;/home/nerf/Zotero/storage/XZQ93HPD/1904.html}
}

@article{riehlINDUCTIVEPRESENTATIONSGENERALIZEDa,
  title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}},
  author = {Riehl, Emily},
  abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.},
  langid = {english},
  file = {/home/nerf/Zotero/storage/6G7N6N5U/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf}
}

@incollection{quillenExamplesSimplicialHomotopy1967,
  title = {Examples of Simplicial Homotopy Theories},
  booktitle = {Homotopical {{Algebra}}},
  author = {Quillen, Daniel G.},
  editor = {Quillen, Daniel G.},
  date = {1967},
  pages = {65--155},
  publisher = {Springer},
  location = {Berlin, Heidelberg},
  doi = {10.1007/BFb0097440},
  url = {https://doi.org/10.1007/BFb0097440},
  urldate = {2024-08-02},
  isbn = {978-3-540-35523-6},
  langid = {english},
  keywords = {Abelian Group,Exact Sequence,Projective Resolution,Simplicial Group,Spectral Sequence},
  file = {/home/nerf/Zotero/storage/SV4WJESD/Quillen - 1967 - Examples of simplicial homotopy theories.pdf}
}

@incollection{quillenAxiomaticHomotopyTheory1967,
  title = {Axiomatic Homotopy Theory},
  booktitle = {Homotopical {{Algebra}}},
  author = {Quillen, Daniel G.},
  editor = {Quillen, Daniel G.},
  date = {1967},
  pages = {1--64},
  publisher = {Springer},
  location = {Berlin, Heidelberg},
  doi = {10.1007/BFb0097439},
  url = {https://doi.org/10.1007/BFb0097439},
  urldate = {2024-08-02},
  isbn = {978-3-540-35523-6},
  langid = {english},
  keywords = {Double Coset,Homotopy Category,Homotopy Theory,Model Category,Weak Equivalence},
  file = {/home/nerf/Zotero/storage/WIV7ECSM/Quillen - 1967 - Axiomatic homotopy theory.pdf}
}

@book{quillenHomotopicalAlgebra1967a,
  title = {Homotopical {{Algebra}}},
  author = {Quillen, Daniel G.},
  editor = {Dold, A. and Eckmann, B.},
  editortype = {redactor},
  date = {1967},
  series = {Lecture {{Notes}} in {{Mathematics}}},
  volume = {43},
  publisher = {Springer},
  location = {Berlin, Heidelberg},
  doi = {10.1007/BFb0097438},
  url = {http://link.springer.com/10.1007/BFb0097438},
  urldate = {2024-08-02},
  isbn = {978-3-540-03914-3 978-3-540-35523-6},
  keywords = {algebra,homotopical algebra,Homotopie,homotopy,homotopy theory,Quillen},
  file = {/home/nerf/Zotero/storage/6JP38TF2/Quillen - 1967 - Homotopical Algebra.pdf}
}

@online{hoveyModelCategories2007a,
  title = {Model {{Categories}}},
  author = {Hovey, Mark},
  date = {2007-10-17},
  series = {Mathematical {{Surveys}} and {{Monographs}}},
  volume = {63},
  publisher = {American Mathematical Society},
  issn = {0076-5376, 2331-7159},
  doi = {10.1090/surv/063},
  url = {https://www.ams.org/surv/063},
  urldate = {2024-08-02},
  abstract = {Advancing research. Creating connections.},
  isbn = {9780821843611 9781470412906},
  langid = {english},
  organization = {American Mathematical Society}
}

@online{awodeyCartesianCubicalModel2023,
  title = {Cartesian Cubical Model Categories},
  author = {Awodey, Steve},
  date = {2023-07-14},
  eprint = {2305.00893},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.2305.00893},
  url = {http://arxiv.org/abs/2305.00893},
  urldate = {2024-08-03},
  abstract = {The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.},
  pubstate = {prepublished},
  keywords = {18N40 18B25 18N45,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/KWCXVX7B/Awodey - 2023 - Cartesian cubical model categories.pdf;/home/nerf/Zotero/storage/PNTHDEYX/2305.html}
}

@article{hofmannLiftingGrothendieckUniverses1997,
  title = {Lifting {{Grothendieck Universes}}},
  author = {Hofmann, Martin and Streicher, Thomas},
  date = {1997-21},
  url = {https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf},
  langid = {english},
  file = {/home/nerf/Zotero/storage/LE9B8IMD/Hofmann et al. - Lifting Grothendieck Universes.pdf}
}

@article{gambinoPolynomialFunctorsPolynomial2013,
  title = {Polynomial Functors and Polynomial Monads},
  author = {Gambino, Nicola and Kock, Joachim},
  date = {2013-01},
  journaltitle = {Mathematical Proceedings of the Cambridge Philosophical Society},
  shortjournal = {Math. Proc. Camb. Phil. Soc.},
  volume = {154},
  number = {1},
  eprint = {0906.4931},
  eprinttype = {arXiv},
  eprintclass = {math},
  pages = {153--192},
  issn = {0305-0041, 1469-8064},
  doi = {10.1017/S0305004112000394},
  url = {http://arxiv.org/abs/0906.4931},
  urldate = {2024-08-04},
  abstract = {We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.},
  keywords = {18C15 18D05 18D50 03G30,Mathematics - Category Theory},
  file = {/home/nerf/Zotero/storage/JMIDZIWR/Gambino and Kock - 2013 - Polynomial functors and polynomial monads.pdf;/home/nerf/Zotero/storage/CADCALSE/0906.html}
}

@article{lackAdhesiveQuasiadhesiveCategories2005,
  title = {Adhesive and Quasiadhesive Categories},
  author = {Lack, Stephen and Sobociński, Paweł},
  date = {2005},
  journaltitle = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
  volume = {39},
  number = {3},
  pages = {511--545},
  issn = {1290-385X},
  doi = {10.1051/ita:2005028},
  url = {http://www.numdam.org/item/ITA_2005__39_3_511_0/},
  urldate = {2024-08-07},
  langid = {english},
  file = {/home/nerf/Zotero/storage/Y3K26BM6/Lack and Sobociński - 2005 - Adhesive and quasiadhesive categories.pdf}
}

@online{hazratpour2categoricalProofFrobenius2024,
  title = {A 2-Categorical Proof of {{Frobenius}} for Fibrations Defined from a Generic Point},
  author = {Hazratpour, Sina and Riehl, Emily},
  date = {2024-02-22},
  eprint = {2210.00078},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.2210.00078},
  url = {http://arxiv.org/abs/2210.00078},
  urldate = {2024-08-08},
  abstract = {Consider a locally cartesian closed category with an object I and a class of trivial fibrations, which admit sections and are stable under pushforward and retract as arrows. Define the fibrations to be those maps whose Leibniz exponential with the generic point of I defines a trivial fibration. Then the fibrations are also closed under pushforward.},
  pubstate = {prepublished},
  keywords = {18N45 18N40 03B38 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
  file = {/home/nerf/Zotero/storage/ISNC6YKS/Hazratpour and Riehl - 2024 - A 2-categorical proof of Frobenius for fibrations .pdf;/home/nerf/Zotero/storage/BIR588ML/2210.html}
}
