A Toolkit for Structured Lifts
Chris Kapulkin, Yufeng Li
TL;DR
The paper develops a theory of structured lifts to model uniform solutions to lifting problems in categorical models of dependent type theory without the heavy algebraic weak factorization framework. It introduces lifting structures including uniform lifts, left/right restrictions, base-change rebasing, structured pushout-product approximations, and structured Leibniz transposes, proving closure, stability, and uniqueness properties. The framework is developed in locally cartesian closed categories and CwRs, with slice- and universe-based formulations to support axiomatization of computation rules in cubical type theory. By enabling restriction, composition, base-change, and relational comparison of lifts under minimal assumptions, it provides a robust toolkit for modeling pattern matching and interactions of dependent sums and path types in type-theoretic semantics.
Abstract
We develop a general framework for working with structured lifting problems, establishing closure and uniqueness properties of their solutions. In a subsequent paper, we apply these results to axiomatize computation rules of cubical type theory.