Bicategorical type theory: semantics and syntax

Authors

Benedikt Ahrens, Paige Randall North, Niels van der Weide

Type: Article

Publication Date: 2023-10-17

Citations: 1

DOI: https://doi.org/10.1017/s0960129523000312

View Ask PDF

Abstract

Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories . Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.

Locations

Mathematical Structures in Computer Science
View PDF
arXiv (Cornell University)
View PDF
Research Repository (Delft University of Technology)
View PDF
Radboud Repository (Radboud University)
View PDF

Ask a Question About This Paper

Summary

Formalizing Monoidal Categories and Actions for Syntax with Binders

2023-01-01

Benedikt Ahrens , Ralph Matthes , Kobe Wullaert

We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq … We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a type-theoretic proof assistant with decidable typechecking) made us use more theory or helped us to see theory more clearly.

View PDF Chat

Implementing a category-theoretic framework for typed abstract syntax

2022-01-11

Benedikt Ahrens , Ralph Matthes , Anders Mörtberg

In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof … In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant. In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply-typed case. As it turns out, in many cases our mechanized results carried over to the generalized definitions without any code change. Second, an existing mechanized library on $\omega$-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bicategorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using a recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly. The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation.

View PDF Chat

Category Theory in Coq 8.5

2016-06-01

Amin Timany , Bart Jacobs

We report on our experience implementing category theory in Coq 8.5. Our work formalizes most of basic category theory, including concepts not covered by existing formalizations, in a library that … We report on our experience implementing category theory in Coq 8.5. Our work formalizes most of basic category theory, including concepts not covered by existing formalizations, in a library that is fit to be used as a general-purpose category-theoretical foundation. Our development particularly takes advantage of two features new to Coq 8.5: primitive projections for records and universe polymorphism. Primitive projections allow for well-behaved dualities while universe polymorphism provides a relative notion of largeness and smallness. The latter is one of the main contributions of this paper. It pushes the limits of the new universe polymorphism and constraint inference algorithm of Coq 8.5. In this paper we present in detail smallness and largeness in categories and the foundation they are built on top of. We furthermore explain how we have used the universe polymorphism of Coq 8.5 to represent smallness and largeness arguments by simply ignoring them and entrusting them to the universe inference algorithm of Coq 8.5. We also briefly discuss our experience throughout this implementation, discuss concepts formalized in this development and give a comparison with a few other developments of similar extent.

A type theory for cartesian closed bicategories (Extended Abstract)

2019-06-01

Marcelo Fiore , Philip Saville

We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies … We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategori-fication of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories.

View PDF Chat

Relative full completeness for bicategorical cartesian closed structure

2021-03-23

Philip Saville , Marcelo Fiore

The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages.Here we extend the construction to accommodate '2-dimensional theories' … The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages.Here we extend the construction to accommodate '2-dimensional theories' of types, terms between types, and rewrites between terms.Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of cartesian closed structure on a glueing category.As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equational theory of rewriting in the fragment with finite products only.

View PDF Chat

A type theory for cartesian closed bicategories

2019-01-01

Marcelo Fiore , Philip Saville

We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies … We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategorification of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories.

Intersection Type Distributors

2021-06-29

Federico Olimpieri

We study a family of distributors-induced bicategorical models of λ-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras … We study a family of distributors-induced bicategorical models of λ-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

View PDF Chat

Definitional Functoriality for Dependent (Sub)Types

2023-01-01

Théo Laurent , Meven Lennon-Bertrand , Kenji Maillard

Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional … Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws, equations satisfied propositionally by a large class of container-like type constructors $F : \mathrm{Type} \to \mathrm{Type}$, equipped with a $\mathrm{map}_{F} : (A \to B) \to F\,A \to F\,B$, such as lists or trees. Promoting these equations to definitional ones strengthens the theory, enabling slicker proofs and more automation for functorial type constructors. This extension is used to modularly justify a structural form of coercive subtyping, propagating subtyping through type formers in a map-like fashion. We show that the resulting notion of coercive subtyping, thanks to the extra definitional equations, is equivalent to a natural and implicit form of subsumptive subtyping. The key result of decidability of type-checking in a dependent type system with functor laws for lists has been entirely mechanized in Coq. This is the extended version of the work with the same name published at ESOP'24.

View PDF Chat

Intersection Type Distributors

2020-02-04

Federico Olimpieri

We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras … We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

Intersection Type Distributors

2020-01-01

Federico Olimpieri

View PDF Chat

Deriving Category Theory from Type Theory

1993-01-01

Roy L. Crole

The Theory of Parametricity in Lambda Cube (Towards new interaction between category theory and proof theory)

2001-06-01

泉竹内

The Theory of Parametricity in Lambda Cube (Towards new interaction between category theory and proof theory)

2001-06-01

Izumi Takeuti

Category Theory in Coq 8.5

2015-05-24

Amin Timany , Bart Jacobs

We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at this https URL This implementation most notably makes use of … We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at this https URL This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.

idris-ct: A Library to do Category Theory in Idris

2020-09-14

Fabrizio Genovese , Alex Gryzlov , Jelle Herold +4 more

We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to … We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business. Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties.

View PDF Chat

idris-ct: A Library to do Category Theory in Idris.

2019-01-01

Fabrizio Genovese , Alex Gryzlov , Jelle Herold +4 more

Complete Bidirectional Typing for the Calculus of Inductive Constructions

2021-01-01

Meven Lennon-Bertrand

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and checking, dubbed constrained inference, to … This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.

View PDF Chat

Multi-dimensional Type Theory: Rules, Categories, and Combinators for Syntax and Semantics

2004-01-01

Jørgen Villadsen

We investigate the possibility of modelling the syntax and semantics of natural language by constraints, or rules, imposed by the multi-dimensional type theory Nabla. The only multiplicity we explicitly consider … We investigate the possibility of modelling the syntax and semantics of natural language by constraints, or rules, imposed by the multi-dimensional type theory Nabla. The only multiplicity we explicitly consider is two, namely one dimension for the syntax and one dimension for the semantics, but the general perspective is important. For example, issues of pragmatics could be handled as additional dimensions. One of the main problems addressed is the rather complicated repertoire of operations that exists besides the notion of categories in traditional Montague grammar. For the syntax we use a categorial grammar along the lines of Lambek. For the semantics we use so-called lexical and logical combinators inspired by work in natural logic. Nabla provides a concise interpretation and a sequent calculus as the basis for implementations.

A Graphical Interface for Category Theory Proofs in Coq

2025-05-07

Luc Chabassier

Relative induction principles for type theories

2021-01-01

Rafaël Bocquet , Ambrus Kaposi , Christian Sattler

We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into … We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over the codomain of F. We rely on the internal language of presheaf categories. In order to combine the internal languages of multiple presheaf categories, we use Dependent Right Adjoints and Multimodal Type Theory. Categorical gluing is used to prove these induction principles, but it not visible in their statements, which involve a notion of model without context extensions. As example applications of these induction principles, we give short and boilerplate-free proofs of canonicity and normalization for some small type theories, and sketch proofs of other metatheoretic results.

Two-sided cartesian fibrations of synthetic $$(\infty ,1)$$-categories

2024-06-21

Jonathan Weinberger

Introduction to bicategories

1967-01-01

Jean Bénabou

Characterization of bicategories of stacks

1982-01-01

Ross Street

The groupoid model refutes uniqueness of identity proofs

2002-12-17

Martin Hofmann , Thomas Streicher

We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements which are not even prepositionally … We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements which are not even prepositionally equal. This shows that the principle of uniqueness of identity proofs is not derivable in the syntax.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>

Fibred and Cofibred Categories

1966-01-01

John W. Gray

Some properties of Fib as a fibred 2-category

1999-01-01

Claudio Hermida

Fibred 2-categories and bicategories

2013-11-25

Mitchell Buckley

View PDF Chat

Fibrations and partial products in a 2-category

1993-01-01

Peter Johnstone

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition … We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

View PDF Chat

Two-dimensional models of type theory

2009-07-02

Richard Garner

We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories. We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

View PDF Chat

Stack semantics of type theory

2017-06-01

Thierry Coquand , Bassel Mannaa , Fabian Ruch

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an … We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

View PDF Chat

A type theory for synthetic ∞-categories

2017-12-22

Emily Riehl , Michael Shulman

We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe … We propose foundations for a synthetic theory of $(\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 \emph{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 \emph{Rezk types}, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities --- a ``local univalence'' condition. And we define \emph{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.

Weak omega-categories from intensional type theory

2010-09-17

Peter LeFanu Lumsdaine

We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. … We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.

View PDF Chat

A type theory for cartesian closed bicategories (Extended Abstract)

2019-06-01

Marcelo Fiore , Philip Saville

View PDF Chat

High-level methods for homotopy construction in associative n-categories

2019-06-01

David Reutter , Jamie Vicary

A combinatorial theory of associative n-categories has recently been proposed, with strictly associative and unital composition in all dimensions, and the weak structure arising as a notion of `homotopy' with … A combinatorial theory of associative n-categories has recently been proposed, with strictly associative and unital composition in all dimensions, and the weak structure arising as a notion of `homotopy' with a natural geometrical interpretation. Such a theory has the potential to serve as an attractive foundation for a computer proof assistant for higher category theory, since it allows composites to be uniquely described, and relieves proofs from the bureaucracy of associators, unitors and their coherence. However, this basic theory lacks a high-level way to construct homotopies, which would be intractable to build directly in complex situations; it is not therefore immediately amenable to implementation. We tackle this problem by describing a `contraction' operation, which algorithmically constructs complex homotopies that reduce the lengths of composite terms. This contraction procedure allows building of nontrivial proofs by repeatedly contracting subterms, and also allows the contraction of those proofs themselves, yielding in some cases single-step witnesses for complex homotopies. We prove correctness of this procedure by showing that it lifts connected colimits from a base category to a category of zigzags, a procedure which is then iterated to yield a contraction mechanism in any dimension. We also present homotopy.io, an online proof assistant that implements the theory of associative n-categories, and use it to construct a range of examples that illustrate this new contraction mechanism.

View PDF Chat

Towards a Directed Homotopy Type Theory

2019-11-01

Paige Randall North

In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types

View PDF Chat

A Constructive Model of Directed Univalence in Bicubical Sets

2020-05-26

Matthew Weaver , Daniel R. Licata

Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based … Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete fibrations whose directed morphisms correspond to functions---a higher-categorical analogue of the category of sets and functions. In this paper, we give a constructive model of a directed type theory with directed univalence in bicubical, rather than bisimplicial, sets. We formalize much of this model using Agda as the internal language of a 1-topos, following Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete fibrations, with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we refine the universe of covariant fibrations using the constructive sheaf models by Coquand and Ruch.

View PDF Chat

Types are weak <i>ω</i> -groupoids

2010-10-12

Benno van den Berg , Richard Garner

We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower … We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.

View PDF Chat

Cartesian closed 2-categories and permutation equivalence in higher-order rewriting

2013-09-04

Tom Hirschowitz

We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete. We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete.

View PDF Chat

The simplicial model of Univalent Foundations (after Voevodsky)

2021-03-08

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky’s construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky’s construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

View PDF Chat

Bicategories in univalent foundations

2021-11-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

View PDF Chat

Semantics for two-dimensional type theory

2022-08-02

Benedikt Ahrens , Paige Randall North , Niels van der Weide

We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory … We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.

View PDF Chat

A type-theoretical definition of weak ω-categories

2017-06-01

Eric Finster , Samuel Mimram

We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself … We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.

View PDF Chat

A Type Theory for Strictly Unital ∞-Categories

2022-08-02

Eric Finster , David Reutter , Jamie Vicary +1 more

We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, … We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.

View PDF Chat