Mu tilde (re)cycled
summary
Proves coherence for cyclic operads by building a mu calculus that merges two decomposition syntaxes, showing every composition order yields the same operation. Uses three concrete syntaxes (edge contractions, node-first, mixed mu syntax), orients rules into a rewriting system, and shows normal forms = blue node‑first forms and anti‑normal = red edge contractions. Key claims: the mixed mu syntax collapses proofs to the two local equations, linearity prevents duplication, and the equational proof closes the coherence theorem.
AI-written summary · about
chapters (8)
- 0:00Start
- 0:44Unrooted Trees
- 2:26The Cyclic Operat
- 2:51Internal Edges and Leaves
- 5:58The Coherence Theorem
- 6:16Indirect Proof
- 12:00The Third Theorem
- 15:16Remarks
related talks
20mModal Mu-Calculus for Free in Agda
29mMechanized monadic equational reasoning for ML references
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
17mDenotation-based Compositional Compiler Verification
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
14mAdequacy for Algebraic Effects Revisited
24mTowards a Higher-Order Mathematical Operational Semantics
15mLiberating Merges via Apartness and Guarded Subtyping