A Toolkit for Structured Lifts
arXiv:2512.14988
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.
33 pages; comments very welcome