Showing 1–2 of 2 results for author: Dean, C J

Computads for weak $ω$-categories as an inductive type

Authors: Christopher J. Dean, Eric Finster, Ioannis Markakis, David Reutter, Jamie Vicary

Abstract: We give a new description of computads for weak globular $ω$-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of $ω$-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every… ▽ More We give a new description of computads for weak globular $ω$-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of $ω$-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every $ω$-category is equivalent to a free one, and that the category of computads with generator-preserving maps is a presheaf topos, giving a direct description of the index category. We prove that our resulting definition of $ω$-category agrees with that of Batanin and Leinster and that the induced notion of cofibrant replacement for $ω$-categories coincides with that of Garner. △ Less

Submitted 20 March, 2024; v1 submitted 18 August, 2022; originally announced August 2022.

Journal ref: Advances in Mathematics 450 (2024), no. 109739

Globular Multicategories with Homomorphism Types

Authors: Christopher J. Dean

Abstract: We introduce a notion of globular multicategory with homomorphism types. These structures arise when organizing collections of "higher category-like" objects such as type theories with identity types. We show how these globular multicategories can be used to construct various weak higher categorical structures of types and terms. We introduce a notion of globular multicategory with homomorphism types. These structures arise when organizing collections of "higher category-like" objects such as type theories with identity types. We show how these globular multicategories can be used to construct various weak higher categorical structures of types and terms. △ Less

Submitted 28 May, 2020; originally announced May 2020.

Comments: 25 pages