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.
Keywords: lifting problems, Leibniz transpose, pushout-product, cubical type theory
2020 MSC: 18A05, 18A15, 18A30, 18A32
Theory and Applications of Categories, Vol. 45, 2026, No. 19, pp 717-758.
Published 2026-03-30.
TAC Home