Homotopy Type Theory for Sewn Quilts
summary
A new imperative language called PieceWork models quilts as shapes built from edges, implements three core operations—mark, cut, sew—and ships a prototype plus examples and an operational semantics; shapes require at least three edges and cuts only split propositionally equivalent points. The paper proves that cut and sew are quasi-inverses at the semantics level, the type system is still in progress, the project is funded, and the prototype matches the intended topological behavior while aiming to generalize beyond quilts.
AI-written summary · about
chapters (16)
- 0:00Homotopy type theory for quilts
- 0:22Why quilts matter
- 1:48Quilting challenges
- 3:11Quilting vs homotopy analogy
- 4:14Homotopy spaces intro
- 5:59Univalence axiom
- 7:24Higher inductive types
- 8:27Peacework language
- 9:30Basic syntax and quilting operations
- 10:10Shapes in Peacework
- 11:34Marking operation
- 12:59Cutting operation
- 14:43Sewing operation
- 15:46Cut and sew inverses
- 16:49Future work on Peacework
- 17:11Question and answer session begins
related talks
14mQUILT: Supporting Modular Design of Machine-Knitting Programs
39mBuilding composable abstractions
16mBecoming Creative: How I Designed a Quilt with R- 16mBecoming Creative: How I Designed a Quilt with R
25mCubical Synthetic Homotopy Theory
41mSuper-fun with First-class Shapes in Quil
41mLanguages for 3D Industrial Knitting
19mIll-Typed Programs Don't Evaluate