Homotopical inverse diagrams in categories with attributes

DOI10.1016/J.JPAA.2020.106563zbMath1453.18007arXiv1808.01816OpenAlexW3084104479MaRDI QIDQ2207273

Krzysztof Kapulkin, Peter LeFanu Lumsdaine

Publication date: 22 October 2020

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

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

zbMATH Keywords

categories with attributeshomotopical inverse diagrams

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Type theory (03B38)

Uses Software

• UniMath

Cites Work

• The identity type weak factorisation system
• On the strength of dependent products in the type theory of Martin-Löf
• The homotopy theory of type theories
• Categories with families and first-order logic with dependent sorts
• The Local Universes Model
• Types are weak ω -groupoids
• Two-dimensional models of type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Abstract homotopy theory and generalized sheaf cohomology
• Homotopy limits in type theory
• Univalence for inverse diagrams and homotopy canonicity
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Homotopical inverse diagrams in categories with attributes