Related papers: A Formal Logic for Formal Category Theory (Extende…
We develop some basic concepts in the theory of higher categories internal to an arbitrary $\infty$-topos. We define internal left and right fibrations and prove a version of the Grothendieck construction and of Yoneda's lemma for internal…
We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types…
This paper proposes an alternative to standard first-order logic that seeks greater naturalness, generality, and semantic self-containment. The system removes the first-order restriction, avoids type hierarchies, and dispenses with external…
Completeness proofs in categorical semantics usually proceed by building a syntactic category whose composition is given by substitution. For untyped effectful Call-by-Value languages, this runs into a basic obstacle: there is no canonical…
We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This…
This note is a survey on the basic aspects of moduli theory along with some examples. In that respect, one of the purposes of this current document is to understand how the introduction of stacks circumvents the non-representability problem…
We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the…
The rules governing the essentially algebraic notion of a category with families have been observed (independently) by Steve Awodey and Marcelo Fiore to precisely match those of a representable natural transformation between presheaves.…
Propositional type theory, first studied by Henkin, is the restriction of simple type theory to a single base type that is interpreted as the set of the two truth values. We show that two constants (falsity and implication) suffice for…
Internal categories feature notions of limit and completeness, as originally proposed in the context of the effective topos. This paper sets out the theory of internal completeness in a general context, spelling out the details of the…
This paper presents a construction which transforms categorical models of additive-free propositional linear logic, closely based on de Paiva's dialectica categories and Oliva's functional interpretations of classical linear logic. The…
We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying…
We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The…
We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of…
Additive categories play a fundamental role in mathematics and related disciplines. Given an additive category equipped with a biadditive functor, one can construct its category of extensions, which encodes important structural information.…
Inductive and coinductive types are commonly construed as ontological (Church-style) types, denoting canonical data-sets such as natural numbers, lists, and streams. For various purposes, notably the study of programs in the context of…
It is a classical theorem that the free product of ordered groups is orderable. In this note we show that, using a method of G. Bergman, an ordering of the free product can be constructed in a functorial manner, in the category of ordered…
Motivated by potential applications to theoretical computer science, in particular those areas where the Curry-Howard correspondence plays an important role, as well as by the ongoing search in pure mathematics for feasible approaches to…
This paper develops a systematic framework for integrating local categories that model logical connectives using higher category theory. By extending these local categories into a unified two-category enriched with natural isomorphisms, the…
In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the…