Related papers: Type theories in category theory
In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories \`a la Martin-L\"of can be interpreted using fibrations. Modern theorem…
Forking is a central notion of model theory, generalizing linear independence in vector spaces and algebraic independence in fields. We develop the theory of forking in abstract, category-theoretic terms, for reasons both practical (we…
This paper introduces Relational Type Theory (RelTT), a new approach to type theory with extensionality principles, based on a relational semantics for types. The type constructs of the theory are those of System F plus relational…
This article is the first in a series of articles that explain the formalization of a constructive model of cubical type theory in Nuprl. In this document we discuss only the parts of the formalization that do not depend on the choice of…
These expanded lecture notes are based on a tutorial on categorical proof theory presented at the summer school associated with the conference "Topology, Algebra, and Categories in Logic 2021-2022." The chapter delves into various…
The recent trend in mathematics is towards a framework of abstract mathematical objects, rather than the more concrete approach of explicitly defining elements which objects were thought to consist of. A natural question to raise is whether…
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not…
This paper proposes a way to compute the meanings associated with sentences with generic noun phrases corresponding to the generalized quantifier most. We call these generics specimens and they resemble stereotypes or prototypes in lexical…
Let $T$ be a (first order complete) dependent theory, ${\mathfrak{C}}$ a $\bar\kappa$-saturated model of $T$ and $G$ a definable subgroup which is abelian. Among subgroups of bounded index which are the union of $<\bar\kappa$ type definable…
The first part of this dissertation defines "dependently typed algebraic theories", which are a strict subclass of the generalised algebraic theories (GATs) of Cartmell. We characterise dependently typed algebraic theories as finitary…
We generalize proarrow equipments from strict category theory to the $\infty$-categorical setting, introducing the concept of $\infty$-equipments. These are specific double $\infty$-categories that support an internal higher category…
There exists a dispute in philosophy, going back at least to Leibniz, whether is it possible to view the world as a network of relations and relations between relations with the role of objects, between which these relations hold, entirely…
Category theory can be used to state formulas in First-Order Logic without using set membership. Several notable results in logic such as proof of the continuum hypothesis can be elegantly rewritten in category theory. We propose in this…
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric hom-types. We articulate…
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this…
The growing complexity of modern practical problems puts high demands on the mathematical modelling. Given that various models can be used for modelling one physical phenomenon, the role of model comparison and model choice becomes…
We define a notion which contains numerous basic notions of Analysis as special cases, for example limit, continuity, differential, Riemann and Lebesgue integral, root and exponential functions. Properties like additivity or linearity of…
We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L\"{o}f type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates…
We present here definitions and constructions basic for the theory of monoidal and tensor categories. We provide references to the original sources, whenever possible. Group-theoretical categories are used as examples
Formalized $1$-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have "higher structure," rely on…