Displayed Categories

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

Authors: Benedikt Ahrens, Peter Lefanu Lumsdaine 

Publication date: 26 May 2020

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

Recommendations

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

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 (5)

• Displayed categories
• 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

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)