Displayed Categories

DOI10.4230/LIPICS.FSCD.2017.5MaRDI QIDQ5111300zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Displayed categories
• Bicategories in univalent foundations
• Categorical notions of fibration
• Constructions of categories of setoids from proof-irrelevant families

Cites work

• scientific article; zbMATH DE number 195102 (Why is no real title available?)
• scientific article; zbMATH DE number 7204300 (Why is no real title available?)
• Basic Category Theory
• Categorical logic and type theory
• Comprehension categories and the semantics of type dependency
• Homotopy type theory. Univalent foundations of mathematics
• Univalent categories and the Rezk completion

Cited in

(5)

• Displayed categories
• Movable categories
• High-level signatures and initial semantics
• Univalent Foundations and the Equivalence Principle
• scientific article; zbMATH DE number 7559271 (Why is no real title available?)

Describes a project that uses

Uses Software

• GitHub
• UniMath
• Coq

This page was built for publication: Displayed Categories

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