scientific article; zbMATH DE number 7559271

DOI10.4230/LIPIcs.FSCD.2019.5MaRDI QIDQ5089004

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

Publication date: 18 July 2022

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Coqdependent type theoryunivalent mathematicsbicategory theory

Mathematics Subject Classification ID

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

Related Items (2)

The construction of set-truncated higher inductive types ⋮ Bicategories in univalent foundations

Cites Work

• Unnamed Item
• Unnamed Item
• Two-dimensional monad theory
• Finitary higher inductive types in the groupoid model
• Natural models of homotopy type theory
• Discrete Generalised Polynomial Functors
• Introduction to bicategories
• Internal type theory
• Categorical structures for type theory in univalent foundations
• Displayed Categories
• The law of excluded middle in the simplicial model of type theory
• A Type-Theoretical Definition of Weak {\omega}-Categories
• Basic Category Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• 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: