A Toolkit for Structured Lifts

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.