A tutorial implementing fragments of Hegel's Science of Logic in Cubical Agda, following the Lawvere/Schreiber/nLab translation program. The resource offers multiple reading tracks for philosophers, type theorists, and programmers, with chapters building linearly and verified theorems in Agda.