A Toolkit for Structured Lifts
Chris Kapulkin, Yufeng Li
TL;DR
This paper introduces a comprehensive framework for structured lifting problems, proving key properties like closure and uniqueness, which lays the groundwork for future applications in cubical type theory.
Contribution
It presents a novel general framework for structured lifting problems, including proofs of closure and uniqueness, advancing the theoretical foundation for related computational rules.
Findings
Established closure properties of structured lifting solutions
Proved uniqueness of solutions in the framework
Laid groundwork for axiomatizing cubical type theory rules
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics and Applications · Homotopy and Cohomology in Algebraic Topology · Polynomial and algebraic computation