Hegel’s Logic in Cubical Agda

A tutorial implementation of fragments of Hegel’s Science of Logic in Cubical Agda, following the Lawvere/Schreiber/nLab translation program.

New here? The Preface orients you in five minutes — what Hegel was trying to do, what putting him in Agda buys us, and what this book deliberately doesn’t try to capture. The How to read this book guide explains the two-track structure.

Already oriented? Pick your track and jump in:

• Coming from philosophy? Start with Chapter 1 and let the Hegelian-thesis, Context, Intuition, and Reads-as sections carry you. Skim the Math and Code blocks. The Glossary covers every Agda construct in plain English.
• Coming from type theory or programming? Start with Chapter 1 and follow the Math, Code, and Reads-as sections. The Hegelian-thesis blocks are motivation; the Glossary covers any German term.
• Just want the formal goods? Every chapter ends with a “What we verified” block listing the theorems Agda actually checked.

The chapters are linear — each builds on the ones before — but you can skip ahead and flip back as needed.