Semantics for two-dimensional type theory
From MaRDI portal
Recommendations
Cites work
- 2-Dimensional Directed Type Theory
- \textsf{Globular}: an online proof assistant for higher-dimensional rewriting
- A Constructive Model of Directed Univalence in Bicubical Sets
- A type theory for synthetic -categories
- A Type-Theoretical Definition of Weak {\omega}-Categories
- AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS
- Bicategories in univalent foundations
- Biunitary constructions in quantum information
- Canonicity for 2-dimensional type theory
- Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
- Categorical notions of fibration
- Comparing composites of left and right derived functors
- Directed algebraic topology and concurrency. With a foreword by Maurice Herlihy and a preface by Samuel Mimram
- Displayed categories
- Fibred 2-categories and bicategories
- scientific article; zbMATH DE number 3779584 (Why is no real title available?)
- scientific article; zbMATH DE number 269628 (Why is no real title available?)
- scientific article; zbMATH DE number 3305157 (Why is no real title available?)
- Introduction to bicategories
- Some properties of Fib as a fibred \(2\)-category
- Stack semantics of type theory
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- The simplicial model of univalent foundations (after Voevodsky)
- Towards a directed homotopy type theory
- Two-dimensional models of type theory
- Types are weak -groupoids
- Univalent categories and the Rezk completion
- Weak omega-categories from intensional type theory
Cited in
(2)
This page was built for publication: Semantics for two-dimensional type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6649441)
