Semantics for two-dimensional type theory
From MaRDI portal
Publication:6649441
DOI10.1145/3531130.3533334MaRDI QIDQ6649441
Niels van der Weide, Paige Randall North, Benedikt Ahrens
Publication date: 6 December 2024
Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) 2-categories, bicategories, double categories (18N10) Type theory (03B38)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Fibred 2-categories and bicategories
- Comparing composites of left and right derived functors
- 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
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- 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
- AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS
- A Type-Theoretical Definition of Weak {\omega}-Categories
- A Constructive Model of Directed Univalence in Bicubical Sets
- Biunitary constructions in quantum information
- 2-Dimensional Directed Type Theory
- Univalent categories and the Rezk completion
This page was built for publication: Semantics for two-dimensional type theory
