Bicategories in univalent foundations

DOI10.1017/S0960129522000032OpenAlexW4220690388MaRDI QIDQ5055496

Niccolò Veltri, Dan Frumin, Marco Maggesi, Niels van der Weide, Benedikt Ahrens

Publication date: 9 December 2022

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129522000032

zbMATH Keywords

Coqdependent type theoryunivalent mathematicsbicategory theory

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Bicategorical type theory: semantics and syntax

Uses Software

• Coq
• UniMath
• GitHub
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Two-dimensional monad theory
• A coherent approach to pseudomonads
• The simplicial model of univalent foundations (after Voevodsky)
• Finitary higher inductive types in the groupoid model
• Biequivalences in tricategories
• A Categorical Semantics for Inductive-Inductive Definitions
• Displayed Categories
• Natural models of homotopy type theory
• Discrete Generalised Polynomial Functors
• A 2-Categories Companion
• A characterization of pie limits
• Introduction to bicategories
• Internal type theory
• Categorical structures for type theory in univalent foundations
• Identity types and weak factorization systems in Cauchy complete categories
• A Higher Structure Identity Principle
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Subequalizers
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories
• Univalent categories and the Rezk completion

This page was built for publication: Bicategories in univalent foundations