Displayed Categories

DOI10.4230/LIPIcs.FSCD.2017.5zbMath1434.18002OpenAlexW4298363923MaRDI QIDQ5111300

Benedikt Ahrens, Peter LeFanu Lumsdaine

Publication date: 26 May 2020

Full work available at URL: https://hal.inria.fr/hal-01584770

zbMATH Keywords

category theoryCoqdependent type theoryunivalent mathematicscomputer proof assistants

Mathematics Subject Classification ID

Foundations, relations to logic and deductive systems (18A15) Type theory (03B38)

Related Items (3)

Univalent Foundations and the Equivalence Principle ⋮ Unnamed Item ⋮ High-level signatures and initial semantics

Uses Software

• Coq
• UniMath
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Comprehension categories and the semantics of type dependency
• Categorical logic and type theory
• Basic Category Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalent categories and the Rezk completion

This page was built for publication: Displayed Categories