The conatural numbers form an exponential commutative semiring
summary
Claims a first mechanized proof that conatural numbers form an exponential commutative semiring in cubical type theory by formalizing addition, multiplication and exponentiation and their laws including distributivity and exponent laws. Shows naive corecursive definitions fail the guardedness/productivity check, explores an internal-state coiterator that scales poorly, then builds a quotiented embedded language — a mixed higher-inductive coinductive type — and interprets it back to conaturals. Uses univalence to transport the operational record and completes the formalization in Cubical Agda.
AI-written summary · about
chapters (11)
- 0:00Conatural numbers intro
- 1:13Conatural numbers as co-inductive types
- 3:23Exponential semiring goal
- 4:47Naive attempt and termination
- 9:04Guarded core recursion states
- 12:19Danielsson's embedded languages
- 16:44Quotient embedded language
- 19:18Predecessor and operations
- 20:45Isomorphism and equations proof
- 21:29Conclusion and open questions
- 23:30Q&A
related talks
25mFulls Seldom Differ
01h 00mUnconference Coq
01h 08mType Arithmetic and the Yoneda Lemma
21mIntrinsically Correct Algorithms and Recursive Coalgebras
54mCategory Theory Through Functional Programming (part 3/3)
51mCategory Theory for the Working Hacker
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
27mIntrinsically Correct Sorting in Cubical Agda