Bibliography

Primary sources

Hegel, G. W. F. (2010). The Science of Logic. Translated by George di Giovanni. Cambridge University Press. (Originally published 1812–1816.) Section numbers throughout this book (e.g., §134, §1191) refer to this translation. Online hyperlinked version collated at the nLab Science of Logic page.

The Lawvere program

Lawvere, F. W. (1994). “Tools for the advancement of objective logic: closed categories and toposes.” In The Logical Foundations of Cognition, ed. J. Macnamara and G. Reyes, Oxford University Press, pp. 43–56.

Lawvere, F. W. (1997). Toposes of laws of motion. Transcript of a talk in Montreal. pdf

nLab. Science of Logic. Collaborative wiki entry developing the Lawvere translation in detail. ncatlab.org/nlab/show/Science+of+Logic

Recent interpretive work

Protin, C. (2025). Hegel and Modern Topology. arXiv:2501.02367 [math.HO]. Proposes connections between Hegelian moves and topological structures (sheaves, germs, double-negation topology, n-connectivity of ∞-groupoids).

Categorical logic and type theory

Jacobs, B. (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, Volume 141. Elsevier. The standard reference for fibred categories and the base-change adjunctions used in Chapter 6.

Hu, J. Z. S. and Carette, J. (2021). “Formalizing Category Theory in Agda.” In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). The methodological reference for setting up category theory in Agda; informs design decisions like proof-relevant setoids and universe polymorphism.

Abramsky, S. and Tzevelekos, N. (2011). “Introduction to Categories and Categorical Logic.” arXiv:1102.1313 [math.CT].

Awodey, S. and Bauer, A. (2024 draft). Introduction to Categorical Logic. Textbook draft.

Homotopy type theory and Cubical Agda

Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. The HoTT Book. homotopytypetheory.org/book

The agda/cubical library. Version 0.9 of the standard Cubical Agda library. The book imports from Cubical.Core.Primitives and Cubical.Foundations.Prelude. github.com/agda/cubical

Critical and historical

Russell, B. (1945). A History of Western Philosophy. Chapter 22. Contains the famous rejection of Hegel’s system as “obfuscating and in fact nonsensical.” A useful contrast.

Magee, G. A. (2001). Hegel and the Hermetic Tradition. Cornell University Press. Treats the speculative-mystical register of Hegel’s writing.

Heidegger, M. (1958). Hegel and the Greeks. Conference of the Academy of Sciences at Heidelberg, July 26, 1958.