Bicategorical type theory: semantics and syntax
From MaRDI portal
Publication:6149956
DOI10.1017/s0960129523000312arXiv2201.10662OpenAlexW4387704456MaRDI QIDQ6149956
Benedikt Ahrens, Paige Randall North, Niels van der Weide
Publication date: 5 March 2024
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2201.10662
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Fibred 2-categories and bicategories
- Some properties of Fib as a fibred \(2\)-category
- The simplicial model of univalent foundations (after Voevodsky)
- Towards a directed homotopy type theory
- Categorical notions of fibration
- Directed algebraic topology and concurrency. With a foreword by Maurice Herlihy and a preface by Samuel Mimram
- Weak omega-categories from intensional type theory
- Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
- Canonicity for 2-dimensional type theory
- Types are weak ω -groupoids
- A type theory for synthetic $\infty$-categories
- Displayed Categories
- Globular: an online proof assistant for higher-dimensional rewriting
- Two-dimensional models of type theory
- Introduction to bicategories
- Bicategories in univalent foundations
- A Type-Theoretical Definition of Weak {\omega}-Categories
- A Constructive Model of Directed Univalence in Bicubical Sets
- 2-Dimensional Directed Type Theory
- Univalent categories and the Rezk completion
This page was built for publication: Bicategorical type theory: semantics and syntax
