Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking.

We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

Computational linguistics studies natural language in its various manifestations from a computational point of view, both on the theoretical level (modeling grammar modules dealing with natural language form and meaning, and the relation between these two) and on the practical level (developing applications for language and speech technology). Right from the start in the 1950s, there have been strong links with computer science, logic, and many areas of mathematics - one can think of Chomsky's contributions to the theory of formal languages and automata, or Lambek's logical modeling of natural language syntax. The symposium on Logic and Algorithms in Computational Linguistics 2021 (LACompLing2021) assesses the place of logic, mathematics, and computer science in present day computational linguistics. It is a forum for presenting new results as well as work in progress.

Higher inductive typesare a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the synthetic development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion ofcell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category hasweakly stable typal initial algebrasfor any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (infinity, 1)-category is presented by some model category to which our results apply.

Classically, any structure for a signature may be completed to a model of a desired regular theory by means of the chase construction or small object argument. Moreover, this exhibits as weakly reflective in .

We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflectivity principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e., set) models.

Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to 'a category D and functor F : D -> C', but instead of having a single collection of 'objects of D' with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

We construct a left semi-model structure on the category of intensional type theories (precisely, on CxlCat(Id,1,Sigma(,Pi ext))). This presents an infinity-category of such type theories; we show moreover that there is an infinity-functor Cl-infinity from there to the infinity-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.

This paper continues investigations in “synthetic homotopy theory”: the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory.

We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations.

The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.