Lean 4 formalization of fixed-point constructions in monoidal closed categories, with computability theory (Myhill isomorphism, Rogers isomorphism, Kleene recursion). 42 files, 8051 lines, 0 custom axioms.
category-theory formal-verification computability-theory mathlib lean4 fixed-point-theorem myhill-isomorphism rogers-isomorphism adamek-theorem
-
Updated
Mar 5, 2026 - Lean