Bicategories in univalent foundations

DOI10.4230/LIPICS.FSCD.2019.5MaRDI QIDQ5089004zbMATH OpenFDO

Authors Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide

Publication date 18 July 2022

Full work available at URL https://arxiv.org/abs/1903.01152

zbMATH Keywords

bicategory theoryCoqdependent type theoryunivalent mathematics

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Recommendations

• Bicategories in univalent foundations
• Univalent categories and the Rezk completion
• Displayed categories
• Univalence in locally Cartesian closed categories
• The simplicial model of univalent foundations (after Voevodsky)

Cites work

• A Type-Theoretical Definition of Weak {\omega}-Categories
• Basic Category Theory
• Categorical structures for type theory in univalent foundations
• Discrete Generalised Polynomial Functors
• Displayed Categories
• Finitary higher inductive types in the groupoid model
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 1289305 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• Internal type theory
• Introduction to bicategories
• Natural models of homotopy type theory
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The law of excluded middle in the simplicial model of type theory
• Two-dimensional monad theory
• Univalent categories and the Rezk completion

Cited in

(12)

• Finitary birepresentations of finitary bicategories
• The construction of set-truncated higher inductive types
• scientific article; zbMATH DE number 6945020 (Why is no real title available?)
• scientific article; zbMATH DE number 7352262 (Why is no real title available?)
• Degrees of bi-embeddable categoricity
• Bicategories in univalent foundations
• The Univalence Axiom in posetal model categories
• scientific article; zbMATH DE number 7774236 (Why is no real title available?)
• Bicategories in Univalent Foundations
• Semantics for two-dimensional type theory
• A Cartesian bicategory of polynomial functors in homotopy type theory
• Universal algebra in UniMath

This page was built for publication: Bicategories in univalent foundations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089004)