A toolkit for structured lifts

MaRDI QIDQ7234760zbMATH OpenFDO

Authors Krzysztof Kapulkin, Yufeng Li

Publication date 29 April 2026

Published in Theory and Applications of Categories (Search for Journal in Brave)

Full work available at URL http://www.tac.mta.ca/tac/volumes/45/19/45-19abs.html

zbMATH Keywords

cubical type theoryLeibniz transposelifting problemspushout-product

Mathematics Subject Classification ID

Definitions and generalizations in theory of categories (18A05) Foundations, relations to logic and deductive systems (18A15) Limits and colimits (products, sums, directed limits, pushouts, fiber products, equalizers, kernels, ends and coends, etc.) (18A30) Factorization systems, substructures, quotient structures, congruences, amalgams (18A32)

Cites work

• A general framework for the semantics of type theory
• Algebraic model structures
• Algebraic weak factorisation systems. I: Accessible AWFS.
• Comprehension categories and the semantics of type dependency
• Effective Kan fibrations in simplicial sets
• Generalized algebraic theories and contextual categories
• Homotopy theoretic models of identity types
• scientific article; zbMATH DE number 5219541 (Why is no real title available?)
• Internal type theory
• Natural models of homotopy type theory
• Natural weak factorization systems.
• Syntax and models of Cartesian cubical type theory
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• The identity type weak factorisation system
• The simplicial model of univalent foundations (after Voevodsky)
• Understanding the small object argument
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: A toolkit for structured lifts

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