Displayed Categories

zbMath1419.18001arXiv1705.04296MaRDI QIDQ3121521

Peter LeFanu Lumsdaine, Benedikt Ahrens

Publication date: 18 March 2019

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

zbMATH Keywords

category theoryCoqdependent type theoryunivalent mathematicscomputer proof assistants

Mathematics Subject Classification ID

Foundations, relations to logic and deductive systems (18A15)

Related Items (7)

The construction of set-truncated higher inductive types ⋮ Bicategories in univalent foundations ⋮ Unnamed Item ⋮ Bicategorical type theory: semantics and syntax ⋮ What should a generic object be? ⋮ Unnamed Item ⋮ Displayed Categories

Uses Software

• Coq
• UniMath
• GitHub

Cites Work

• Unnamed Item
• Isomorphism is equality
• Categorical logic and type theory
• The Local Universes Model
• Displayed Categories
• Categorical structures for type theory in univalent foundations
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalent categories and the Rezk completion

This page was built for publication: Displayed Categories