Displayed Categories

DOI10.4230/LIPICS.FSCD.2017.5zbMATH Open1434.18002OpenAlexW4298363923MaRDI QIDQ5111300FDOQ5111300

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)

Cites Work

• Categorical logic and type theory
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Comprehension categories and the semantics of type dependency
• Basic Category Theory
• Univalent categories and the Rezk completion
• Title not available (Why is that?)

Cited In (4)

• Movable categories
• High-level signatures and initial semantics
• Univalent Foundations and the Equivalence Principle
• Title not available (Why is that?)

Uses Software

• Coq
• UniMath
• GitHub

   Recommendations

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

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)