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.

Preface

What this book is

This is a literate Cubical Agda program that walks through fragments of G.W.F. Hegel’s Science of Logic (1812–1816). Each chapter pairs a Hegelian move with a verified type-theoretic construction. Every claim that is not explicitly flagged as a postulate is checked by the Agda typechecker — what you read is what the compiler accepted.

The translation framework is the one developed by William Lawvere and refined collaboratively on the nLab, identifying Hegelian concepts (Concept, Judgment, Moment, Aufhebung, the adjoint triple Possibility–Actuality–Necessity) with constructions from categorical logic and homotopy type theory.

What is Hegel trying to do?

The Science of Logic is Hegel’s attempt to derive every category of thought from no presupposition at all. He begins from Pure Being — the emptiest possible concept — and shows that each category, examined honestly, reveals an internal tension that forces the move to the next. By the end, Being has become Quantity, Quantity has become Essence, and Essence has become the Absolute Idea, with every step justified by what came before. The wager is that the categories of thought are not a static list to be enumerated, but a self-developing sequence — and that following the development is logic.

The engine of that development is a move classical logic treats as a defect: contradiction. Hegel argues that contradictions, taken seriously instead of explained away, are the productive moments where thought moves forward. Pure Being collapses into Pure Nothing not because Hegel made a mistake but because thinking each one honestly leads, by itself, to the other. Out of that collapse comes Becoming, and from Becoming the whole rest of the system. If the move from Being to Nothing fails, the Logic fails at step one. If it succeeds, the categories aren’t arbitrary cultural artifacts — they’re the shape thought had to take.

Why formalize?

Putting Hegel into Agda forces a kind of honesty that prose can’t. Every “transition” becomes either a verified construction — we built it; the typechecker accepted it — or an explicit caveat: here is where the formal version stops short of Hegel’s claim, and here is what we still gain anyway. The reader sees, line by line, which parts of the dialectical machinery survive translation and which don’t.

That is worth doing whether you came to convince yourself Hegel is formalizable or to convince yourself he isn’t. The caveats are called out at every point where Hegel says more than the formalization can. Where the formalization succeeds, the proof is on the page. Where it falls short, the gap is named and the reader gets to weigh it.

What this book is not

• It is not a complete formalization of Hegel. Six short chapters cover a fragment of Volume 1 (the Doctrine of Being) and the opening of Volume 2 (the Doctrine of Essence). The Doctrine of the Notion, the Doctrine of Actuality in detail, and much else, are not covered.
• It is not an original mathematical contribution. The Lawvere/nLab translation is the source of all the ideas. The implementation is a careful, pedagogical realization of a program that has been articulated elsewhere.
• It is not a defense of the claim that Hegel can be formalized. The claim is contested — Hegel himself argues in §1798 that consistent formal logic cannot capture the productive contradictions central to his system. We try to be explicit at each step about what is captured and what is not.

The two tracks

Each chapter is structured so that a philosophy reader can read just the Hegelian-thesis, Context, Intuition, and Reads-as sections and walk away with the argument; a programmer reader can read just the Math, Code, and Reads-as sections and walk away with the construction. The “Reads as” paraphrases are the bridge present in both tracks.

If you don’t know either side, How to read this book explains the structure in more detail.

What you need

• No prior Agda knowledge. Syntax is introduced as it appears. The shared Cubical primitives reference collects everything Agda-specific in one place.
• No prior Hegel. German terms are glossed in the Glossary. Section numbers (e.g., §134) refer to the di Giovanni translation of the Science of Logic (Cambridge University Press, 2010), which is also the edition cited on the nLab Science of Logic page.

Acknowledgments

The translation framework this book implements is due principally to William Lawvere; its current articulation is collaborative work on the nLab. Recent suggestions about how Hegelian concepts surface in topology and homotopy theory come from Clarence Protin’s 2025 paper Hegel and Modern Topology. The Agda implementation benefits from agda/cubical and the wider Agda community’s work on Cubical Agda.

The honest framing of “what is and isn’t captured” owes a great deal to several rounds of internal review during drafting.

Contact & contributing

Questions, corrections, pushback, and collaboration are all welcome.

• Errata, typos, technical issues — open an issue at github.com/ddebruce/hegel-agda/issues.
• Discussion of the philosophy or formalization — github.com/ddebruce/hegel-agda/discussions. Specific is more useful than general: “Chapter 4 §3 paragraph 2” beats “Chapter 4 was confusing.”
• Serious correspondence (collaboration, citation, review) — hello@ddebruce.com.

I am especially interested in: places where the Lawvere/nLab translation feels strained, candidates for a non-trivial Aufhebung instance, and Doctrine-of-the-Notion material I have not yet attempted.

How to read this book

The book is structured to serve two distinct readers at once.

Hegel’s Logic is simultaneously a formal system and a piece of philosophy — the categorical and the conceptual co-develop, and neither makes much sense alone. The two tracks honor that split: the philosophy track follows the conceptual argument, the programmer track follows the formal construction, and the “Reads as” paraphrases bridge them. Most readers benefit from peeking at the other track now and then.

Each chapter section uses some subset of these facets, each at whatever length the pedagogy demands:

• Hegelian thesis — what Hegel claims, in his terms, with citations to the §§ of the Science of Logic.
• Context — where the move sits in the dialectical arc.
• Intuition — the picture, example, motivating analogy.
• Math — the categorical or type-theoretic content.
• Code — the Agda.
• Reads as — a natural-language bridge between code and concept.

Not every section uses every facet. The discipline is: a reader should be able to skim the facets foreign to their background and still come away with what was claimed and whether it was verified.

If you come from philosophy

Your track is Hegelian thesis → Context → Intuition → Reads as.

You can skim or skip the Math and Code blocks. The “Reads as” paraphrase tells you what the code is claiming, phrased as a Hegelian assertion. If you want a quick check on whether a chapter verified something, look for the “What we verified” block at the end of every chapter.

If you encounter an Agda symbol you want to understand briefly, the Glossary explains every construct used in the book in plain English. The Cubical primitives appendix collects the more technical pieces and is meant for look-up, not first-read.

If you come from type theory or programming

Your track is Math → Code → Reads as.

You can skim the Hegelian-thesis sections, treating them as motivation. The German terms get glossed; if you’re not sure what Aufhebung or Wirklichkeit mean, the Glossary covers them.

The book uses Cubical Agda. If you know plain Agda but not the cubical extension, the Cubical primitives reference brings you up to speed in one page.

If you come from both — or neither

Read everything. The book aims to keep both tracks short enough that reading both is not punishing.

On the order

The chapters are linear: each depends on the ones before. You can skip ahead but you may have to flip back. The “Where we are” header at the start of each chapter reminds you what’s been built so far; the “What’s next” footer points forward.

Chapter 1 — Foundations of Thought

{-# OPTIONS --cubical --guardedness #-}

module ch01-foundations where

Where we are

This is the opening chapter of Hegel’s Logic in Cubical Agda. We start with the three most basic structural pieces of Hegel’s logic — Concepts, Judgments, and the Syllogism — and capture each via its standard correspondent in type theory.

These mappings are Aristotelian — they capture the baseline Hegel begins from. His distinctive moves come later. This chapter shows the baseline working in Agda; subsequent chapters introduce what Hegel adds to it. The point isn’t to defend Aristotelian logic against Hegel; it’s to make the gap Hegel will try to close as crisp as possible — the gap between concepts as static containers and concepts as self-developing wholes.

1. Concepts (Begriffe)

Hegelian thesis

Hegel’s most fundamental unit is the Concept (Begriff). But “concept” here means something more dynamic than the everyday sense. In the Doctrine of the Notion (§1280 ff.) Hegel treats a concept as a self-developing unity of three moments:

• The universal — what the concept means in general. Humanity, justice, redness.
• The particular — the determinate kinds or aspects through which the universal expresses itself. This kind of human, this shade of red.
• The individual — the singular term that is this particular this-universal at once. Socrates, who is both this particular human and an instance of humanity in general.

“Individual” here is philosophical jargon for a singular instance — Socrates, this cup, this proof — not “a person.” The three moments are not three separate things; they are three aspects of one self-moving concept, and Hegel’s claim that they form a real unity is one of the load-bearing claims of the whole Logic.

For this opening chapter we will work with the much weaker static “container” reading — concept-as-type, with individuals as terms of that type — because it is what type theory can capture cleanly. Later chapters introduce the moves that begin to recover Hegel’s richer picture. The reduction is honest about its limits, and we will signal them as they bite.

In code

In Agda, the universe of all concepts is called Set. Despite the name, Set does not mean “set” in the Cantor sense — it just means “type.” The naming is historical.

To make sure we have something concrete to reason about, we postulate the existence of an unspecified concept. postulate is Agda’s keyword for “assume this exists without construction.” We use it sparingly elsewhere in this book; a few abstract starting points are useful.

postulate
  C : Set

Reads as

“Let there be a Concept C — an unspecified type in the universe of all types.”

2. Judgments (Urteile)

Hegelian thesis

A Concept by itself is empty until something is asserted of it. Hegel’s Judgment (Urteil — literally Ur-Teil, “primal division”) is the assertion that an individual belongs to a Concept. In the Doctrine of the Notion Hegel develops four kinds of Judgment (existence, reflection, necessity, the Notion); here we formalize only the most basic — the typing judgment that an individual instantiates a concept.

This identification of philosophical Judgment with typing judgment is the first big stretch. Hegel’s Urteil has rich internal structure that the type-theoretic correspondent flattens. We mark this as a caveat now and develop more of the structure in later chapters.

Caveat: This chapter formalizes only the existential Judgment (c is a C). Hegel’s later Judgments of reflection, necessity, and the Notion (§§1641–1680) are not captured by the bare typing judgment.

In code

The typing judgment in Agda is the colon. Writing c : C means “c is a term of type C.” We postulate one to give the chapter something to reason about.

postulate
  c : C

Reads as

“The individual c is asserted to belong to the concept C.”

3. The Universal Judgment (“All B are A”)

Hegelian thesis

Concepts relate to each other. The simplest relation is universal subsumption: “All Humans are Mortal.” Hegel discusses this in the section on the Judgment of Existence (§§1671 ff.) where the form “All B are A” appears as one of the first relations Concepts can enter into.

In code

In Agda this is the function type. A function f : B → A is a rule that, given any term of type B, produces a term of type A. So “all B are A” becomes “there is a function from B to A” — every B can be transformed into (or revealed to be) an A.

postulate
  A : Set
  B : Set
  f : B → A

Reads as

“Two concepts A and B, and a rule f assigning each individual of B a corresponding individual of A — that is, ‘all B are A’.”

4. The Syllogism (Schluss)

Hegelian thesis

Hegel argues that isolated Judgments are incomplete: they cry out for connection through a mediating middle term. This is the Syllogism (Schluss — “closing” or “conclusion”). The classical example:

“All Humans are Mortal. Socrates is Human. Therefore Socrates is Mortal.”

Three concepts (Mortal, Human, Socrates); the middle term (Human) links the other two. In the Doctrine of the Notion (§§1436 ff.) Hegel surveys three kinds of Syllogism and argues that the Aristotelian form is structurally inadequate. We capture the Aristotelian form here as a baseline; the deeper moves come later.

Math

In categorical terms, the Aristotelian syllogism is composition of functions. Given f : B → A and b : E → B, the composite f ∘ b : E → A is the syllogism’s conclusion. The Curry-Howard correspondence identifies this with the natural-deduction rule of modus ponens applied transitively.

In code

postulate
  E : Set       -- An individual concept (e.g., Socrates)
  b : E → B     -- "All E are B" (e.g., "Socrates is Human")

We now write our first Agda program. Unlike postulate, which merely asserts, this provides an explicit construction. The = gives the definition; λ is “lambda” — Agda’s way of introducing a function by saying “given an input named e, return …”:

syllogism : E → A
syllogism = λ e → f (b e)

The construction reads step by step:

1. We want to produce a term of type E → A.
2. λ e → introduces a placeholder e of type E.
3. b e applies our hypothesis b, yielding a term of type B.
4. f (...) applies f to that, yielding a term of type A.
5. The composite is the function we sought. Agda verifies the types at every step.

Reads as

“To produce an A from any E: take e, apply b to reveal it as a B, then apply f to that B to arrive at an A.”

What we verified

In this chapter, Agda has checked these constructions:

• syllogism : E → A exists, derived from f : B → A and b : E → B by function composition.

The other declarations (C, c, A, B, f, E, b) are postulates — assumed, not verified. We use postulates here only to have abstract starting points; subsequent chapters drop postulates in favor of real proofs.

What we now know that we didn’t before: the Aristotelian baseline of Hegelian logic — concept, judgment, syllogism — maps cleanly to type theory, but the mapping treats concepts as static containers. The gap between concept-as-container and Hegel’s three-moment self-moving concept is the gap the rest of the book tries to close.

What’s next

After Chapter 1 we have a vocabulary — Concept — and a minimal syntax — Judgment, Universal Judgment, Syllogism. What we don’t have is anything to say with it. The postulates A, B, C, c are abstract placeholders standing in for concepts that, so far, have no content.

The next move in the Science of Logic is to ask: what is the simplest possible concept? What can we say if we presuppose nothing at all? Hegel’s answer is Pure Being (das Sein) — the concept of being-as-such, with every determination stripped away. Chapter 2 follows that move, introduces also Pure Nothing (das Nichts), and discovers the first dialectical turn: the two seemingly opposite concepts collapse into each other, and out of that collapse comes Becoming (das Werden) — the first concrete category. The whole rest of the Logic unfolds from this opening move.

Chapter 2 — The Logic of Being

{-# OPTIONS --cubical --guardedness #-}

module ch02-being where

Where we are

Chapter 1 introduced Concepts (types), Judgments (typing), and the Syllogism (function composition). Those Concepts were postulated — we never asked “what is the simplest possible Concept?”

The Science of Logic begins not with the syllogism but with the pair Pure Being (Sein) and Pure Nothing (Nichts). Hegel argues these are equally indeterminate, and their tension gives rise to Becoming (Werden). Here we set up the type-theoretic correspondents:

What’s at stake

Pure Being is not picked out of a hat. Hegel chooses it as the starting point because it presupposes nothing: every other concept (a chair, a number, justice — anything determinate) carries content that would have to be justified having smuggled in. Pure Being carries no content. It’s where you start if you want a logic with no foreign assumptions.

The whole Science of Logic depends on what happens next. If thought can move at all from Pure Being to its opposite without importing external content — if Being collapses into Nothing just by being thought through honestly — then the categories of thought are self-generating and the dialectical engine is real. If thought can’t make that move, the entire programme stalls at step one.

Said more directly: Hegel is trying to give a logical account of how something arises from nothing. Why is there something rather than nothing at all? You can’t answer that question without a way to derive determinate content from sheer indeterminacy. Chapter 2 is where the derivation either starts or fails.

1. Pure Being (Das Sein)

Hegelian thesis

Hegel’s Pure Being is the most abstract concept possible: pure existence without any further qualities. “X is” — said of nothing in particular and without further specification.

The Science of Logic opens with this concept (§132). Hegel emphasizes that Pure Being has no determinations whatsoever: no content, no internal distinction, no relation. It is the absolute beginning precisely because it presupposes nothing.

Intuition

A type-theoretic correspondent should be a type that “just is” — inhabited, but trivially. The natural choice: a type with exactly one inhabitant, where the inhabitant carries no information. That is the unit type, traditionally written ⊤ (“top”).

In code

Agda’s record keyword defines a type whose values are tuples of fields. A record with no fields and a single constructor tt is inhabited by exactly one value.

record ⊤ : Set where
  constructor tt

Reads as

“Pure Being ⊤ is the type whose sole inhabitant is tt, with no further data.”

2. Pure Nothing (Das Nichts)

Hegelian thesis

Hegel’s Pure Nothing is the categorical opposite of Pure Being: the concept under which nothing falls. He insists that Pure Nothing is not merely “the absence of being” but a positive thinking of the non-being itself.

The Science of Logic asserts that Pure Nothing has the same indeterminacy as Pure Being. Both lack any qualities. This is already the seed of the dialectical move to come — but we develop that in Section 3.

In code

In type theory the categorial opposite of “one inhabitant” is “no inhabitants.” We declare a type with data and provide no constructors. There is then no way to build a term of type ⊥, and under propositions-as-types, ⊥ is the proposition that is provably false.

data ⊥ : Set where
  -- (intentionally no constructors)

Reads as

“Pure Nothing ⊥ is the type with no inhabitants whatsoever.”

3. Becoming (Das Werden)

Hegelian thesis

Hegel’s central early move: Being and Nothing are equally indeterminate, so they “pass over into each other.” Their truth is Becoming — the movement between them (§134 ff.). The famous formulation is that Sein and Nichts are identical in their truth.

This is the move the chapter promised. If it works, Hegel has begun answering the deepest question of the Logic: how does determinate content arise from sheer indeterminacy? Becoming is the first determinate concept — the first something — and it is generated by the tension between two indeterminate ones. No external content was imported; the movement is internal to thought itself.

Caveat: This chapter only models the form of the transition — two functions, one in each direction. The much stronger claim that Sein and Nichts are identical is formalized in Chapter 4 using a Higher Inductive Type. Consistent formal logic cannot make ⊤ and ⊥ judgmentally equal, so the identification will happen at the path level rather than the equation level. (See Higher Inductive Types for the relevant Cubical primitive.)

Why this matters: for Hegel, the process is the philosophy. It is not just that Being and Nothing turn out to be identical — it is that thought discovers their identity by working through the contradiction. The collapse is the dialectical move. Our formal version, by contrast, gives the destination (a path-identification, in Chapter 4) without the journey. This is the place a reader skeptical of formalizing Hegel will plant their flag, and they are not wrong to do so. We accept the gap openly: what we capture is the result the contradiction is meant to produce, not the productive contradiction itself.

Intuition

For now, a first weak way to model the transition: any type X sits “between” ⊥ and ⊤, because there is a unique function ⊥ → X (the principle of explosion: from nothing, anything follows) and a unique function X → ⊤ (any determinate thing can be stripped of its qualities and reduced to bare existence).

        ⊥ ───── from-nothing ─────▶ X ───── to-being ─────▶ ⊤

These functions exist for trivial categorical reasons (⊥ is initial, ⊤ is terminal in the category of types). They carry no information in themselves — Chapter 4 will give the transition real content.

In code

The function from Nothing into any type uses the absurd pattern (). This tells Agda: “there are no inhabitants of ⊥ to consider, so this function is defined everywhere it needs to be defined (which is nowhere).”

from-nothing : {X : Set} → ⊥ → X
from-nothing ()

The function to Being throws away its input and returns the unique inhabitant of ⊤:

to-being : {X : Set} → X → ⊤
to-being x = tt

Reads as

From ⊥: “From the empty type, a function to any type X exists vacuously — there is nothing to map, so every case is handled.”

To ⊤: “Any term of type X collapses to the featureless point of Pure Being.”

What we verified

In this chapter, Agda has checked these constructions:

• ⊤ is well-formed as a unit type with sole inhabitant tt.
• ⊥ is well-formed as an uninhabited type.
• from-nothing : {X : Set} → ⊥ → X typechecks — the principle of explosion is a real Agda function.
• to-being : {X : Set} → X → ⊤ typechecks — the unique map to the terminal type is constructed explicitly.

What we now know that we didn’t before: the structural form of Hegel’s opening move has a type-theoretic shape — ⊤, ⊥, and the bare arrows between them and any type. What we have is the destination of the Sein-Nichts collapse; what we do not have yet, and what Chapter 4 reaches for, is its dialectical content.

What’s next

Chapter 3 replaces our postulates with real proofs, introduces paths from Cubical Agda, and begins to give the bare construction of “Becoming” real content. We will see the first place the --cubical pragma earns its keep: a proof that Pure Being is contractible, which is much stronger than “has one inhabitant.”

Chapter 3 — Determinate Being

{-# OPTIONS --cubical --guardedness #-}

module ch03-determinate-being where

open import ch02-being
open import Cubical.Core.Primitives

Where we are

Chapter 2 set up Pure Being (⊤), Pure Nothing (⊥), and the bare arrows ⊥ → X and X → ⊤ that gave a first, weak gesture at Becoming. Every nontrivial claim in that chapter was a postulate or a one-line definition — nothing we constructed required Cubical Agda’s machinery.

This chapter moves from asserted by postulate to verified by proof, and introduces our first genuinely Cubical content. We produce three concrete results, each genuinely checked by Agda:

1. ⊤ is contractible — strictly stronger than “has one inhabitant,” and the first place we use a path explicitly.
2. The curry/uncurry adjunction (A × B → C) ≃ (A → B → C) — our first non-trivial adjunction, witnessed by explicit programs.
3. The unit of double negation X → ¬¬X — the first concrete example of a modal operator, foreshadowing the Moment record of Chapter 4.

What’s at stake

Chapters 1 and 2 were almost entirely scaffolding: postulated concepts, bare arrows, and the suggestion of a dialectical move that the formalization deferred. This chapter is where both halves of the project turn concrete.

On the Hegelian side: Pure Being has collapsed. From here on, we develop determinate concepts — concepts with actual content that survive the collapse and stand on their own. (Hegel’s term is Dasein, “being-there,” and the move is the bridge from sheer abstract Being to anything one could actually point at.) The chapter does not trace the full Hegelian arc through Quality and Quantity — those are large parts of the Logic we explicitly defer — but it does the parallel formal move.

On the type-theoretic side: postulates give way to proofs. Cubical Agda’s paths give us the machinery to identify things that aren’t judgmentally equal, to show isomorphisms between types, and to model operators that act on types. Each of the three sections below is an explicit construction the typechecker accepts.

The shared thread is content from no content. Chapter 2 promised that determinate concepts could be derived without external assumptions. This chapter makes good on that promise three times: contractibility (Pure Being is internally as identical as a thing can be), curry/uncurry (a real adjunction with verified inverses), and the double-negation modality (our first concrete modal operator).

Prelude: Cubical primitives

Cubical Agda extends Agda with primitives from Cubical Type Theory. We import them from the official cubical library. Detailed reference: Cubical primitives.

The key import is Cubical.Core.Primitives, which gives us:

• _≡_ — the path/equality type
• refl — the constant path, witnessing x ≡ x
• PathP — dependent paths (used internally)
• Σ, _,_ — dependent pairs

In Cubical Type Theory, x ≡ y is not a static fact but a path between x and y in a type viewed as a space. A path is a function from the unit interval I = [i0, i1] into the type, with endpoints x and y. The syntax λ i → ... defines a path by giving its value at each point i of the interval. Σ and its constructor _,_ come transitively from Agda.Builtin.Sigma via the cubical library, so no local redefinition is needed.

1. Pure Being is Contractible

Hegelian thesis

Hegel emphasizes throughout the opening of the Science of Logic that Pure Being has no internal distinction: no content, no qualities, no relation, no movement of its own. It is pure self-identity, undifferentiated from itself in every respect.

Chapter 2 captured the one-inhabitant aspect of this with ⊤, but mere singleness is too weak. A type with one inhabitant only says x = y for any two points. Hegel’s claim is stronger: there is no distinguishable structure at any level. The right formal correspondent is contractibility — pure self-identity all the way up.

Math

A type A is contractible when there is a center point x : A such that every other point y has a path to x. Path equality means: any two inhabitants are identified — and because paths between paths are themselves data in Cubical Type Theory, contractibility says these higher-order identifications are also connected, and so on indefinitely up the homotopy hierarchy.

A set with one element merely satisfies x = y. A contractible type additionally satisfies that all paths between its points are themselves connected, paths between those paths are connected, and so on. Contractibility is therefore strictly stronger than “has one inhabitant.”

In code

The definition uses Σ to package a center together with the contraction proof:

isContr : Set → Set
isContr A = Σ A (λ x → (∀ y → x ≡ y))

For ⊤, the center is tt. Because records with one constructor enjoy automatic eta-equality, any y : ⊤ is judgmentally equal to tt, so the constant path λ i → tt witnesses tt ≡ y:

⊤-is-contractible : isContr ⊤
⊤-is-contractible = (tt , λ y → (λ i → tt))

Reads as

“Pure Being is contractible: its center is tt, and any other inhabitant is identified with tt by the constant path.”

2. A real categorical adjunction (Product ⊣ Exponential)

Math

An adjunction in category theory is a precise sense in which two operations are “inverse up to isomorphism.” Hegel uses unity of opposites for a related move in philosophy; we will formalize that connection in Chapter 4.

The currying isomorphism is the most famous adjunction in logic. It says: a function on pairs A × B → C is “the same data” as a function A → B → C that expects its arguments one at a time. This is our first non-trivial adjunction — the cartesian-closed structure of types — and it foreshadows the broader “unity of opposites = adjunction” theme developed in the next chapter.

In code

First, a minimal pair type. (Cubical’s library has a richer one; this minimal version is for clarity.)

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

curry : {A B C : Set} → (A × B → C) → (A → B → C)
curry f = λ a b → f (a , b)

uncurry : {A B C : Set} → (A → B → C) → (A × B → C)
uncurry f = λ p → f (p ._×_.fst) (p ._×_.snd)

These two functions witness the adjunction (- × B) ⊣ (B → -). They are not postulates: they are explicit programs that Agda compiles and that perfectly invert each other.

Reads as

“Functions on pairs and functions taking arguments one at a time are interchangeable.”

3. Negation and the double negation modality

Hegelian thesis

Negation is structural in Hegel: the determinate emerges from Pure Being by being marked off against what it is not. And the “negation of the negation” is the engine of dialectic itself — the move by which a determination, by being negated and that negation in turn negated, returns to itself enriched.

We cannot yet model the full dialectical movement, but we can formalize the operator that double negation describes. Modeling “X and not-not-X are related but not identical” is exactly the intuitionistic situation, and exactly the right preparation for the modal-operator pattern Chapter 4 will generalize.

Math

In intuitionistic type theory, to negate X means to prove X → ⊥: a function that, given any X, produces a contradiction. Double negation is ¬ (¬ X). Constructively, X → ¬¬X always holds, but ¬¬X → X does not — that direction is the Law of Excluded Middle, which we do not assume.

The functor ¬¬ is our first concrete modal operator: an operation on types that captures a quality (here, “not-not-X-ness”) which classically coincides with X but intuitionistically is strictly weaker. The form X → ◯ X for a functor ◯ is exactly the shape of a monadic unit, and Chapter 4 will abstract this pattern into a Moment record.

Caveat: Hegel’s negation of the negation is not just the operator ¬¬; it is a productive move. For Hegel, negating a determination and then negating that negation does not return to a logically equivalent statement — it produces a new, richer determination that incorporates and surpasses the original. Our formal version captures the operator (X → ¬¬X) but not the productivity.

Why this matters: the gap between X and ¬¬X is exactly where Hegelian dialectical negation might live. Classical logic identifies the two and the gap disappears — so more of Hegel survives here precisely because we work intuitionistically and ¬¬X → X does not hold. The η of a non-trivial modality is the best formal residue available; the productive move itself remains beyond what type theory has yet captured.

In code

¬_ : Set → Set
¬ X = X → ⊥

double-negation-unit : {X : Set} → X → ¬ (¬ X)
double-negation-unit x = λ f → f x

Reads as

“From any x of X, we produce a refutation of the refutation of X — by applying the supposed refutation to x itself.”

What we verified

In this chapter, Agda has checked these constructions:

• ⊤-is-contractible : isContr ⊤ — a real Cubical proof (no postulate) that Pure Being has no internal distinction at any level.
• curry and uncurry — explicit programs witnessing the product/exponential adjunction (- × B) ⊣ (B → -).
• double-negation-unit : {X : Set} → X → ¬ ¬ X — concrete construction of the η of the double-negation modality.

What we now know that we didn’t before: the bare apparatus of Chapter 2 admits real proofs, real adjunctions, and a real modal operator. ⊤ is contractible — not just one-element. Curry/uncurry is a verified adjunction. ¬¬ is the first concrete modality, and the gap between X and ¬¬X is where intuitionism preserves Hegel that classical logic would erase.

What’s next

Chapter 4 puts the pieces together and makes the central Hegelian move available formally. It will:

• Use a Higher Inductive Type to identify Sein and Nichts — the strongest formal expression of Hegel’s claim that Sein and Nichts are identical in their truth.
• Generalize the modal-operator pattern of double negation into a Moment record with full coherence laws.
• Define Unity of Opposites as an adjunction, with explicit inverse proofs.
• Construct the initial opposition ∅ ⊣ * as a verified instance of Unity of Opposites.

Chapter 4 — Unity and Aufhebung

{-# OPTIONS --cubical --guardedness #-}

module ch04-unity-aufhebung where

open import Cubical.Core.Primitives
open import Cubical.Foundations.Prelude using (refl)
open import ch02-being
open import ch03-determinate-being

Where we are

Chapter 2 introduced Pure Being (⊤), Pure Nothing (⊥), and the bare arrows ⊥ → X and X → ⊤ — a first, weak gesture at Becoming with no Cubical content. Chapter 3 added genuine Cubical machinery: contractibility of ⊤, the curry/uncurry adjunction, and the double-negation unit X → ¬¬X — our first concrete modal operator.

This is the most distinctively Hegelian chapter. It makes five moves:

1. Sein ≡ Nichts via HIT. A Higher Inductive Type Becoming contains the points being and nothing plus a path werden : being ≡ nothing identifying them.
2. Moments and Co-Moments with laws. Records that capture monads and comonads — with the coherence laws, not just the signatures.
3. Unity of Opposites as adjunction. A UnityOfOpposites record binding a Co-Moment to a Moment with two inverse proofs.
4. The initial opposition ∅ ⊣ *. A fully-verified instance Becoming-Adjunction : UnityOfOpposites Nothing-CoMoment Being-Moment.
5. Aufhebung as record. The structural form of a higher Unity subsuming a lower one, declared but not yet inhabited.

What’s at stake

Chapters 1–3 set up the apparatus. This chapter is where the apparatus is asked to do real Hegelian work.

Aufhebung — sublation in English — is Hegel’s signature move and the one most readers come to see. Three senses fused in a single word: to cancel, to preserve, to elevate. When a concept is sublated, its contradictions are resolved, its content survives, and it is lifted to a richer determination. This is what makes Hegel’s dialectic forward-moving rather than cyclic. Without Aufhebung, contradictions in thought just oscillate. With it, each contradiction produces the next stage of the system.

The chapter is also where we deploy Cubical Agda’s most distinctive feature — Higher Inductive Types — for a specifically philosophical purpose. The HIT lets us assert an identification (Sein ≡ Nichts) that classical logic would reject, without collapsing into inconsistency. Hegel needs exactly this kind of identification, and classical logic refuses to grant it; cubical type theory gives us the form while honestly flagging what remains beyond reach.

If the chapter succeeds, you walk away with: a path between Pure Being and Pure Nothing, a real verified instance of “unity of opposites” as a categorical adjunction, and a named — though not yet inhabited — structural form for Aufhebung itself.

1. Sein ≡ Nichts (Becoming as a Higher Inductive Type)

Hegelian thesis

Hegel’s most famous early claim in the Science of Logic (§134–§180) is that Pure Being and Pure Nothing are identical in their truth — not approximately, not as a regulative idea, but equal. At §178 he writes that their truth is “this movement of the immediate vanishing of the one in the other”: Becoming (Werden). The two are not merely related opposites side by side — their identity is the dynamic, the passing-over of each into the other, which Hegel will then re-determine as the structure of all subsequent thought.

Caveat: Consistent formal logic cannot make ⊤ and ⊥ judgmentally equal — doing so would yield a term of every type and collapse the system. Hegel himself flags this barrier at §1798: “the thinking of contradiction is the essential moment of the Notion.” No consistent formal system captures Hegel’s claim fully. The Higher Inductive Type below gets us the closest available compromise: a path-level identification, structural rather than judgmental.

Why this matters: without an HIT we would be stuck with two bad choices — accept inconsistency (which destroys the system) or deny the identification (which destroys Hegel’s claim). The HIT carves a third way: the identification is real and constructive, but it lives at the path level rather than the equation level, so it doesn’t collapse ⊤ and ⊥ for every purpose. That is closer to the texture of “the same in their truth, not in their separate appearances” than any classical system can reach. We are postulating exactly the kind of identification Hegel needs — and the system stays consistent.

Math

Higher Inductive Types (HITs) extend ordinary inductive types with path constructors. An ordinary inductive type introduces a type by listing its point constructors (e.g. zero and suc for ℕ). A path constructor introduces, in addition, an explicit identification — a path — between two points of the type. In ordinary type theory this is impossible: equality is propositional and cannot be axiomatised constructor-by-constructor. In Cubical Type Theory it is a basic feature, because paths are themselves first-class data (functions out of the interval I).

A HIT is therefore the natural home for Hegel’s “Sein ≡ Nichts”: we get to put a path between the two points without postulating a contradiction.

In code

data Becoming : Set where
  being   : Becoming
  nothing : Becoming
  werden  : being ≡ nothing

Reads as

“Becoming is a space containing the point being, the point nothing, and a path werden between them — identifying them not by equation but by an explicit continuous transition.”

2. Moments and Co-Moments (Monads and Comonads with laws)

Hegelian thesis

Hegel uses the word Moment not in the temporal sense but as a structural component of a concept — a quality that can be projected out of a concept while remaining tied to it. A Moment is therefore an operator: it takes a concept and exhibits a specific quality of it. The dual is a Co-Moment, which extracts rather than projects.

Chapter 3’s ¬¬ was our first concrete example of this pattern: the operator X ↦ ¬¬X with its unit X → ¬¬X is exactly the shape of a Moment — a functor with an insertion. Here we abstract that pattern, and additionally demand the coherence laws that prevent garbage inhabitants of the record.

Math

Categorically, a Moment is a monad: a functor ◯ equipped with a unit η : X → ◯ X (insertion) and a multiplication μ : ◯ ◯ X → ◯ X (collapse of nesting), satisfying functoriality and the monad laws. A Co-Moment is the comonad dual: a functor ◻ with counit ε : ◻ X → X (extraction) and comultiplication δ : ◻ X → ◻ ◻ X (duplication).

The laws are what give the record real content. The left-unit law says inserting an x and then collapsing gives back x unchanged: “inserting then collapsing is the identity.” The right-unit law says inserting inside an existing ◯ X (by mapping η across it) and then collapsing also gives back the original: “inserting on the inside then collapsing is also the identity.” Functoriality (map-id) says the operator respects identities. Without these laws, any triple of functions with the right type signatures would qualify; with them, only genuine (co)monads inhabit the record.

In code

record Moment : Set₁ where
  field
    -- The functor.
    ◯ : Set → Set
    -- Reads as: "◯ acts on functions, lifting f to a function on ◯."
    map : {X Y : Set} → (X → Y) → ◯ X → ◯ Y
    -- Reads as: "the unit η inserts an X into ◯ X."
    η : {X : Set} → X → ◯ X
    -- Reads as: "the multiplication μ collapses nested ◯ ◯ down to ◯."
    μ : {X : Set} → ◯ (◯ X) → ◯ X
    -- Functor law: map of the identity function is the identity.
    map-id : {X : Set} (x : ◯ X) → map (λ y → y) x ≡ x
    -- Monad law: inserting then collapsing is the identity.
    left-unit  : {X : Set} (x : ◯ X) → μ (η x) ≡ x
    -- Monad law: inserting on the inside then collapsing is also id.
    right-unit : {X : Set} (x : ◯ X) → μ (map η x) ≡ x

A fully-axiomatised monad also requires associativity μ (map μ x) ≡ μ (μ x) and functoriality of composition. We omit these to keep the record manageable; the two instances we construct below satisfy all monad laws trivially.

record CoMoment : Set₁ where
  field
    ◻ : Set → Set
    comap : {X Y : Set} → (X → Y) → ◻ X → ◻ Y
    -- Reads as: "the counit ε extracts an X from ◻ X."
    ε : {X : Set} → ◻ X → X
    -- Reads as: "the comultiplication δ duplicates ◻ X into ◻ (◻ X)."
    δ : {X : Set} → ◻ X → ◻ (◻ X)
    comap-id : {X : Set} (x : ◻ X) → comap (λ y → y) x ≡ x
    left-counit  : {X : Set} (x : ◻ X) → ε (δ x) ≡ x
    right-counit : {X : Set} (x : ◻ X) → comap ε (δ x) ≡ x

3. The Unity of Opposites (Adjoint Moments)

Hegelian thesis

Hegel’s unity of opposites binds a Moment and a Co-Moment together. They are not just two operators standing side by side: each is the other’s counterpart, and their relation has a precise shape. The categorical name for this shape — for the binding of a Moment to a Co-Moment that makes the pair mutually defining — is an adjunction.

Math

An adjunction C ⊣ M between functors is a natural isomorphism

Hom(◻ X, Y) ≃ Hom(X, ◯ Y)

meaning a function ◻ X → Y carries the same data as a function X → ◯ Y, with a bijection that perfectly inverts. We capture this with forward, backward, and the two inverse proofs fwd-bwd and bwd-fwd. The inverse proofs are what prevent garbage inhabitants of the record: any pair of translations that fails to invert is rejected by Agda.

In code

record UnityOfOpposites (C : CoMoment) (M : Moment) : Set₁ where
  field
    forward  : {X Y : Set} → (CoMoment.◻ C X → Y) → (X → Moment.◯ M Y)
    backward : {X Y : Set} → (X → Moment.◯ M Y) → (CoMoment.◻ C X → Y)
    fwd-bwd  : {X Y : Set} (f : X → Moment.◯ M Y) (x : X)
             → forward (backward f) x ≡ f x
    bwd-fwd  : {X Y : Set} (g : CoMoment.◻ C X → Y) (cx : CoMoment.◻ C X)
             → backward (forward g) cx ≡ g cx

A full notion would also demand naturality of forward and backward in both variables. We omit that here for brevity; the instance below is natural by inspection.

Reads as

“A Unity of Opposites is a pair of mutually inverse translations: one direction sends maps out of ◻ X into Y to maps of X into ◯ Y, and the other sends them back, with proofs that each round trip returns the original.”

4. The Initial Opposition (∅ ⊣ *)

Math

We now construct our first instance of UnityOfOpposites — the starting point of Hegel’s whole development. Following the Lawvere/nLab reading of the Science of Logic, the initial opposition is the adjunction between

• the constant comonad at ⊥ — ◻ X = ⊥ for every X — as the left adjoint, representing Nothing, and
• the constant monad at ⊤ — ◯ X = ⊤ for every X — as the right adjoint, representing Being.

It is the foundational categorical structure on which all further determinations of being and essence are built.

Caveat: The adjunction is content-free: both Hom-sets are contractible (any two functions between contractible types are equivalent up to a unique path), so the bijection holds vacuously. That triviality is faithful to the Lawvere reading — the initial opposition IS the bare-minimum categorical structure, and richer dialectical content arrives by further determination, not from this opposition itself.

In code

The constant comonad at ⊥: every field reduces to a vacuous absurd pattern, because ◻ X = ⊥ has no inhabitants for Agda to operate on:

Nothing-CoMoment : CoMoment
Nothing-CoMoment = record
  { ◻ = λ X → ⊥
  ; comap = λ {X} {Y} f ()
  ; ε = λ {X} ()
  ; δ = λ {X} ()
  ; comap-id = λ {X} ()
  ; left-counit = λ {X} ()
  ; right-counit = λ {X} ()
  }

The constant monad at ⊤: all laws are discharged by refl, because ⊤ enjoys eta-equality and so any two of its inhabitants are judgmentally equal to tt:

Being-Moment : Moment
Being-Moment = record
  { ◯ = λ X → ⊤
  ; map = λ {X} {Y} f _ → tt
  ; η = λ _ → tt
  ; μ = λ _ → tt
  ; map-id = λ x → refl
  ; left-unit = λ x → refl
  ; right-unit = λ x → refl
  }

The initial opposition: every required field is a real term, and Agda verifies the inverse proofs. The vacuous cases on the Nothing side use the absurd pattern; the ⊤ side uses refl because ⊤’s eta-equality makes any path between inhabitants definitionally refl:

Becoming-Adjunction : UnityOfOpposites Nothing-CoMoment Being-Moment
Becoming-Adjunction = record
  { forward  = λ f x → tt
  ; backward = λ g ()
  ; fwd-bwd  = λ f x → refl
  ; bwd-fwd  = λ g ()
  }

5. Aufhebung (Sublation)

Hegelian thesis

Hegel’s Aufhebung combines three senses at once: to cancel, to preserve, and to elevate. A sublation cancels the contradiction of a lower Unity, preserves its moments, and raises them to a resolved higher Unity. The lower opposition is not destroyed; its content survives, but as a moment of a richer, more determinate structure.

In code

We model the structural shape: a higher UnityOfOpposites that subsumes a lower one via an inclusion of the lower moment into the higher.

record Aufhebung (C₁ : CoMoment) (M₁ : Moment) : Set₁ where
  field
    sublating-C : CoMoment
    sublating-M : Moment
    sublating-Unity : UnityOfOpposites sublating-C sublating-M
    preserve-elevate : {X : Set} → Moment.◯ M₁ X → Moment.◯ sublating-M X

Caveat: We declare the Aufhebung record but do not construct an instance. The record captures the “contains” aspect (a higher Unity subsumes a lower one) but understates Hegel’s structure — a full account would require the inclusion to commute with the moment operations and would track how the contradiction is resolved at the higher level. A non-trivial Aufhebung instance is on the deferred list, awaiting the richer modalities of later chapters.

Why this matters: the record names what an Aufhebung would have to provide — and naming the shape is itself a real contribution. It says, formally: a sublation is a higher adjunction containing the lower one, plus a structural inclusion of the lower moment. The honest gap is that we have not exhibited a concrete inhabitant. The record only becomes non-trivial when there exists an instance that is not equal to the lower Unity itself, and constructing such an instance is the genuinely philosophical content. (The initial opposition below is too empty to admit one; richer Hegelian moves — Quality from Quantity, Essence from Being — would.) Candidates for v2 are listed at the end of the book. Until then the structural shape is named, the slot is empty, and the reader can see exactly where the philosophical work would have to happen.

Reads as

“An Aufhebung of a lower (C₁ ⊣ M₁) is a higher Unity (sublating-C ⊣ sublating-M) plus a function showing the lower moment is contained in the higher moment.”

What we verified

• Becoming : Set is a Higher Inductive Type with werden : being ≡ nothing — Sein and Nichts identified at the path level, not judgmentally.
• Moment and CoMoment records demand functoriality plus the monad/comonad unit laws — not just the bare signatures, so only genuine (co)monads can inhabit them.
• Being-Moment : Moment and Nothing-CoMoment : CoMoment are constructed; every included law is verified by refl (Being side, via the eta law for ⊤) or by the absurd pattern (Nothing side).
• Becoming-Adjunction : UnityOfOpposites Nothing-CoMoment Being-Moment is constructed with explicit forward, backward, and the two inverse proofs fwd-bwd and bwd-fwd.
• The Aufhebung record is declared, not inhabited — intentionally, as flagged in the caveat above.

What we now know that we didn’t before: Higher Inductive Types let us name Hegel’s signature identification (Sein ≡ Nichts) without collapsing into inconsistency; monads and comonads with laws are the categorical shape of Hegelian Moments; Unity of Opposites is an adjunction with verified inverses. The structural infrastructure of dialectic is in place, even where the genuine philosophical content — a non-trivial Aufhebung — remains the next move.

What’s next

Chapter 5 turns to the Doctrine of Essence (Wesen), the second book of Hegel’s Logic. We move from the bare opposition of ⊥ and ⊤ to the structured universe of mere propositions Ω, and to Reflection — characteristic maps as the categorical correlate of Hegel’s “appearance returning into itself.”

Chapter 5 — The Logic of Essence

{-# OPTIONS --cubical --guardedness #-}

module ch05-essence where

open import Cubical.Core.Primitives
open import ch02-being

Where we are

Chapters 1–4 covered the Doctrine of Being: Concepts, Pure Being (⊤), Pure Nothing (⊥), their path-level identification via a Higher Inductive Type, the framework of Moments and Co-Moments, and the initial opposition ∅ ⊣ *. Throughout, the question driving us was “what is there?” — what shapes inhabit the universe of bare types and bare arrows.

This chapter moves to Hegel’s second book, the Doctrine of Essence (Wesen). The driving question shifts: not “what is there?” but “what is essential?” — meaning, what survives once mere appearance (Schein) is set aside. We are no longer cataloguing types; we are asking which types carry no information beyond their truth value, and assembling those into a register of essences.

Two type-theoretic tools do the work:

1. isProp — a predicate picking out the types where any two inhabitants are connected by a path. These are the “essential” types: they discard all internal variation.
2. Ω — the type of all propositions, the “register of essences.” Topos-theoretically this is the subobject classifier; here it is also our home for Reflection, characteristic maps X → Ω.

What’s at stake

The Doctrine of Being asked: what is there? — what shapes inhabit the universe of types and arrows. The Doctrine of Essence asks something different: what is essential? — what survives once mere appearance is set aside, and what register of kinds of truth are concepts answerable to.

The structural shift is from concepts that simply are (immediate categories like Being, Nothing, Becoming) to concepts that reflect on themselves to find their truth. A reflective concept turns back into itself, sorts its surface qualities into what’s accidental and what’s essential, and discovers its truth not by reaching outward to a definition but by recovering itself from its own appearances. That is the move Reflection (Reflexion, §§814 ff.) names.

This chapter is where Hegel’s logic stops being “moves between categories” and starts being “categories thinking about themselves.” We capture the proposition-level fragment of that move — three small pieces that fit together:

• isProp picks out the types whose internal variation has been collapsed: the essential types.
• Ω collects those types into a register — a universe of essences a concept can be mapped into.
• A Reflection is the mapping itself: a function X → Ω that recognizes, for each x : X, which essence it belongs to.

1. Propositions (Essential Truths)

Hegelian thesis

In the Doctrine of Essence, Hegel contrasts essence (Wesen) with appearance (Schein). At §818 he frames essence as what is left when mere appearance is set aside — the truth of being that has gone into itself, no longer scattered across surface qualities but gathered into a self-relation. A concept’s essence is what remains invariant when all its accidental differences are quotiented out.

Type-theoretically, this is exactly what isProp captures: a type is a proposition when its internal variation has been collapsed, so any two inhabitants are equally good — the type carries nothing beyond its mere being-true.

Math

In Homotopy Type Theory, a type A is a proposition when any two of its inhabitants are connected by a path. This means A has at most one “way to be true” — it carries no information beyond its truth value.

• ⊤ is a proposition: it has exactly one inhabitant, trivially identified with itself.
• ⊥ is a proposition: it has no inhabitants at all, so the identification is vacuous.
• Bool (the type with two distinct inhabitants true and false) is not a proposition: there is no path between true and false.

Propositions are the “essential” types: their internal structure has been discarded in favor of pure truth value.

In code

isProp : Set → Set
isProp A = (x y : A) → x ≡ y

⊤-is-prop : isProp ⊤
⊤-is-prop x y = λ i → tt

⊥-is-prop : isProp ⊥
⊥-is-prop ()

Reads as

“A type A is a proposition when any two of its elements are connected by a path.”

“Pure Being is essentially without distinction: any two of its points are identified — eta-equality makes both judgmentally equal to tt, so the constant path λ i → tt connects them.”

“Pure Nothing is essentially without distinction vacuously: there are no inhabitants whose distinction could arise, and the absurd pattern handles the (impossible) input.”

2. Ω, the type of propositions

Hegelian thesis

For Hegel, essence is not something hidden behind appearance — it is reflection within itself (§816, §834). Essence appears as appearance to itself: it is the movement by which a concept returns into itself from its surface determinations and recognizes those determinations as its own. The universe of essences is therefore not a remote interior; it is the structured space in which each concept finds its truth.

Mathematically, we model that structured space as Ω: the type whose inhabitants are precisely the propositions, each paired with its certificate of being-essential.

Caveat: Ω collects only the proposition-level “essences.” It is not the full type universe Type. The Lawvere/nLab reading of Hegel’s “essence as reflection within itself” usually points at the full type universe (made reflective by univalence). Here we capture the proposition-level fragment of that — mathematically cleaner, and what we actually need for this chapter’s purposes.

Why this matters: Hegel’s essence is about the whole shape of conceptual content — not just yes/no truth values but the rich internal structure of categories, which the Doctrine of the Notion would develop further. Our Ω is the cleanest formal target available: it lets us state Reflection precisely as a characteristic map and verify a non-trivial example against it. The larger Hegelian programme of “essence-as-reflection across the full universe” awaits univalence-aware constructions we don’t yet build. What we gain here is real and verified — the proposition-level fragment — and we are honest that it is a fragment.

Math

Ω (also written hProp, for “homotopy proposition”) is the type of all propositions. An inhabitant of Ω is a pair: a type, together with a proof that the type is a proposition.

Ω lives in Set₁ because its inhabitants are pairs whose first component is itself a Set. (A type whose values include types must live one universe level up.)

Topos-theoretically, Ω is the subobject classifier: every “subset” of a type X corresponds to a function X → Ω giving the characteristic predicate for membership. This is the role we exercise in Section 3.

In code

record Ω : Set₁ where
  constructor prop
  field
    carrier : Set
    essence : isProp carrier

True-Essence : Ω
True-Essence = prop ⊤ ⊤-is-prop

False-Essence : Ω
False-Essence = prop ⊥ ⊥-is-prop

Reads as

“Ω contains, for each carrier type, a proof that the carrier is a proposition. Inhabiting Ω is being-essential.”

3. Reflection (Characteristic maps)

Hegelian thesis

Hegel’s Reflection (Reflexion) is a concept’s appearance within the universe of essences — the act by which a concept shows itself in the register of what is essential. A reflection does not invent its content; it sorts the elements of its domain into their essential truths, recognizing which inhabit which essence.

Mathematically a Reflection is a function X → Ω assigning each x its essential truth. Equivalently, a Reflection is a subset of X (the elements mapping to True-Essence) together with the characteristic information that says, for each x, how it belongs.

In code

Reflection : Set → Set₁
Reflection X = X → Ω

all-true : {X : Set} → Reflection X
all-true x = True-Essence

data Bool : Set where
  true  : Bool
  false : Bool

bool-reflect : Reflection Bool
bool-reflect true  = True-Essence
bool-reflect false = False-Essence

Reads as

“A Reflection on X is a rule assigning each x : X to an essence (a proposition in Ω).”

all-true is the trivial Reflection: every element is unconditionally essential, and Ω’s classifying role is not exercised. bool-reflect is the canonical non-trivial example: it distinguishes true from false as characteristic of two different essences, and so actually uses Ω as a classifier rather than as a placeholder.

What we verified

In this chapter, Agda has checked these constructions:

• isProp : Set → Set defines the predicate “any two inhabitants are path-equal.”
• ⊤-is-prop : isProp ⊤ — Pure Being is essentially without distinction.
• ⊥-is-prop : isProp ⊥ — Pure Nothing is essentially without distinction, vacuously.
• Ω : Set₁ is declared as a record with carrier : Set and essence : isProp carrier.
• True-Essence : Ω and False-Essence : Ω populate the register of essences with our two canonical propositions.
• Reflection : Set → Set₁ is defined as X → Ω.
• all-true : {X : Set} → Reflection X — the trivial Reflection that sends everything to True-Essence.
• Bool : Set is declared locally with two constructors true and false.
• bool-reflect : Reflection Bool — the first non-trivial Reflection, which actually exercises Ω’s classifier role by splitting Bool into two distinct essences.

What we now know that we didn’t before: Hegel’s “essence as what survives when appearance is set aside” has a proposition-level formal target. Ω collects the essences. Reflection (X → Ω) recovers a concept’s essential truths from its surface presentations; bool-reflect shows the classifier role is non-trivial. The Doctrine of Essence has a first verified fragment.

What’s next

Chapter 6 introduces Actuality (Wirklichkeit). Following the Lawvere/nLab reading, Hegel’s modalities of Possibility, Actuality, and Necessity correspond to the adjoint triple Σ ⊣ W ⊣ Π in dependent type theory. We construct that triple, prove the adjunctions, and link back to this chapter with a small theorem: Π (Necessity) preserves propositionhood — the universe of essences Ω is closed under necessitation.

Chapter 6 — Actuality

{-# OPTIONS --cubical --guardedness #-}

module ch06-actuality where

open import Cubical.Core.Primitives
open import Cubical.Foundations.Prelude using (refl)
open import ch02-being
open import ch05-essence

Where we are

Chapter 5 introduced the Doctrine of Essence: isProp, the type Ω of all propositions, and Reflection as a characteristic map X → Ω. We asked “what is essential?” and gathered the answers into a register of essences.

This chapter moves to Hegel’s Doctrine of Actuality (Wirklichkeit). At §1191 of the Science of Logic Hegel treats modality as a trio — Possibility, Actuality, Necessity — each the truth of the last. Following the Lawvere/nLab reading, this trio corresponds to an adjoint triple of base-change operations in dependent type theory: Σ ⊣ W ⊣ Π. Modality is not a single operator but a structured chain of three.

We construct each of the three operations, prove the two adjunctions with their inverse maps, and link back to Chapter 5 by showing that Π preserves propositionhood — the universe of essences is closed under necessitation.

What’s at stake

Actuality is a hinge in Hegel. It’s the moment where essence becomes effective — where the inner truth developed in the Doctrine of Essence shows up as outer reality. In the structure of the Logic, Actuality is also where the Doctrine of Essence ends and the Doctrine of the Notion begins. (We do not enter the Notion in this book.) In the larger system, Actuality is the bridge from logic to nature and spirit — the moment where the self-developing conceptual structure connects with what is.

Two things are at stake formally. First, that Hegel’s triad Possibility / Actuality / Necessity has a verified type-theoretic counterpart at all. Following the Lawvere/nLab reading, that counterpart is the adjoint triple Σ ⊣ W ⊣ Π. Finding a triadic structure that mirrors Hegel — and verifying both adjunctions — is non-trivial evidence for the Lawvere program: triadic structures are everywhere in Hegel, and a clean formal one matters.

Second, that the Doctrine of Actuality is compatible with the Doctrine of Essence. If Necessity destroyed essences, the system would be incoherent. The chapter closes by proving the bridge theorem — Π-preserves-prop — so the universe of essences is closed under necessitation. The book ends with the two doctrines formally cohering.

1. Actuality as weakening (Truth in a Context)

Hegelian thesis

Hegel’s Actuality (Wirklichkeit) places a truth into a concrete context. A truth that is actual is not an abstract or floating proposition — it is one that holds here, at every point of the situation in which we find ourselves. Actuality is the way an unconditioned truth descends into a context and becomes a constant feature of it.

Type-theoretically, this is weakening: taking a value that does not depend on a context A and viewing it as a constant family over A. The value is the same at every point of A, but it is now read as inhabiting that context.

In code

weaken : {A C : Set} → C → (A → C)
weaken c = λ a → c

Reads as

“If C holds absolutely, then C holds at every point of A.”

2. Possibility (Σ, left adjoint to weakening)

Hegelian thesis

Hegel’s Possibility (Möglichkeit) is the modality of mere existence-at-some-point: a concept holds possibly in a context A when there is at least one point of A at which it holds. It is the weakest of the three modalities — to be possible is only to be witnessed somewhere, not everywhere, and not yet to be placed in the situation as actuality is.

Math

In dependent type theory this is the dependent sum Σ A B: a pair of a witness a : A together with a proof of B a. To inhabit Σ A B is to exhibit some a that makes B a true.

Σ is left adjoint to weakening. The adjunction is the equivalence

(Σ A B → C) ≃ ((a : A) → B a → C)

A function from “there exists an a with B a” to C is the same data as a function “for every a, B a implies C.” The two sides of the bijection convert between an existential input and a universal parametrisation.

In code

possibility-forward : {A C : Set} {B : A → Set}
                    → (Σ A B → C) → ((a : A) → B a → C)
possibility-forward f = λ a b → f (a , b)

possibility-backward : {A C : Set} {B : A → Set}
                     → ((a : A) → B a → C) → (Σ A B → C)
possibility-backward g = λ p → g (p .fst) (p .snd)

possibility-fwd-bwd : {A C : Set} {B : A → Set} (g : (a : A) → B a → C)
                    → possibility-forward (possibility-backward g) ≡ g
possibility-fwd-bwd g = λ i → g

possibility-bwd-fwd : {A C : Set} {B : A → Set} (f : Σ A B → C)
                    → possibility-backward (possibility-forward f) ≡ f
possibility-bwd-fwd f = λ i → f

Both compositions reduce judgmentally to the identity, so the constant cubical path λ i → ... witnesses each inverse law.

Reads as

“Mapping out of an existential is the same data as universally consuming both the witness and its proof.”

“Conversely, a function handling every (a, b) pair assembles into a function out of the Σ-type.”

3. Necessity (Π, right adjoint to weakening)

Hegelian thesis

Hegel’s Necessity (Notwendigkeit) is the strongest of the three modalities: a concept holds necessarily in a context A when it holds at every point of A. Necessity does not merely witness; it covers — there is no point of the context that escapes the truth.

Math

In dependent type theory this is the dependent product (a : A) → B a, sometimes written Π A B. To inhabit it is to give, for each a : A, a proof of B a.

Π is right adjoint to weakening. The adjunction is

((a : A) → C → B a) ≃ (C → (a : A) → B a)

A family of functions C → B a (one per a) is the same data as a single function from C into the dependent product.

In code

necessity-forward : {A C : Set} {B : A → Set}
                  → ((a : A) → C → B a) → (C → ((a : A) → B a))
necessity-forward f = λ c a → f a c

necessity-backward : {A C : Set} {B : A → Set}
                   → (C → ((a : A) → B a)) → ((a : A) → C → B a)
necessity-backward g = λ a c → g c a

necessity-fwd-bwd : {A C : Set} {B : A → Set} (g : C → ((a : A) → B a))
                  → necessity-forward (necessity-backward g) ≡ g
necessity-fwd-bwd g = λ i → g

necessity-bwd-fwd : {A C : Set} {B : A → Set} (f : (a : A) → C → B a)
                  → necessity-backward (necessity-forward f) ≡ f
necessity-bwd-fwd f = λ i → f

Reads as

“Giving a function C → B a for each a is the same as giving a single function C → ∀a. B a.”

“The two presentations of a universal family — indexed outside-in or inside-out — carry exactly the same data.”

4. Necessity preserves Essence

Hegelian thesis

If Necessity destroyed Essence — turning essential truths into non-essential ones — the system would be incoherent. A truth that holds necessarily should still be essential: covering every point of a context cannot manufacture spurious internal distinctions. The doctrine of Actuality must be compatible with the doctrine of Essence developed in Chapter 5.

Math

Claim. If B a is a proposition for every a : A, then (a : A) → B a is a proposition.

That is, Necessity (Π) preserves Essence (propositionhood). The proof is one line: at each a, use the proof that B a is a proposition to identify any two functions pointwise.

This connects directly to Chapter 5’s isProp.

Caveat: The Σ ⊣ W ⊣ Π identification with Hegelian Possibility ⊣ Actuality ⊣ Necessity is the dependent-type-theoretic analog of modal Possibility and Necessity (◊, □). Classical modal logic defines those as unary operators on propositions; the dependent-type version generalizes them to operators on dependent types. They coincide on subsingleton (propositional) types and diverge on richer types. The Lawvere reading takes this analogy as the formal residue of Hegel’s distinction.

Why this matters: the divergence is interesting, not a defect. On propositions, our Σ and Π reduce to the familiar existential and universal quantifiers and behave just like modal ◊ and □. On richer types they do more — Σ keeps the witness alongside the proof, Π produces a family of proofs indexed by context — and that extra structure is precisely what the Lawvere reading takes to be the formal residue of Hegel’s distinction. Classical modal logic distinguishes Possibility and Necessity only at the level of truth values; the dependent-type version distinguishes them at the level of content. What it means for Possibility to differ from Necessity as operators on actual dependent content (rather than only on propositions) is an open research question, and our verified triple is a starting point for asking it.

In code

Π-preserves-prop : {A : Set} {B : A → Set}
                 → ((a : A) → isProp (B a))
                 → isProp ((a : A) → B a)
Π-preserves-prop B-prop f g = λ i a → B-prop a (f a) (g a) i

Reads as

“If B a is essentially-without-distinction for every a, then any two universal proofs (a : A) → B a are themselves essentially identified — pointwise, at each a.”

What we verified

In this chapter, Agda has checked these constructions:

• weaken : {A C : Set} → C → (A → C) — Actuality as constant families.
• Four possibility-* terms with both inverse proofs — the Σ ⊣ W adjunction, fully witnessed.
• Four necessity-* terms with both inverse proofs — the W ⊣ Π adjunction, fully witnessed.
• Π-preserves-prop — the cross-chapter bridge: Necessity preserves Essence.

What we now know that we didn’t before: Hegel’s triad Possibility–Actuality–Necessity corresponds to the adjoint triple Σ ⊣ W ⊣ Π, both adjunctions verified with explicit inverses. Necessity preserves Essence (Π-preserves-prop), so the Doctrine of Essence and the Doctrine of Actuality formally cohere. Across the six chapters: where the Lawvere translation survives Hegel, the proof is on the page; where it falls short, the gap is named.

What we built / what we did not build

What we built (across six chapters)

• The basics: Concepts as types, Judgments as typing, Syllogism as composition (Chapter 1).
• Logic of Being: Pure Being (⊤) and Pure Nothing (⊥), the bare arrows for Becoming (Chapter 2).
• Cubical Determinate Being: contractibility of ⊤, the curry/uncurry adjunction, the negation modality (Chapter 3).
• Unity and Aufhebung: Sein ≡ Nichts via HIT, Moments and Co-Moments with laws, Unity of Opposites, the initial opposition ∅ ⊣ * built and verified (Chapter 4).
• Logic of Essence: Propositions, Ω as classifier of essences, Reflection as characteristic map X → Ω (Chapter 5).
• Actuality: the Σ ⊣ W ⊣ Π adjoint triple, with Π preserving propositionhood (this chapter).

What we did not build (deferred)

• A non-trivial Aufhebung instance (the Chapter 4 record is defined but uninhabited).
• The Doctrine of Quality vs. Quantity (the Lawvere program’s differential cohesion).
• The Doctrine of the Notion proper — universality, particularity, individuality as a unity.
• Actual use of the werden path from Chapter 4 — e.g., transporting a function defined on being to one defined on nothing and observing the result.

These are projects for further chapters. The present book is a foundation that can be extended in any of these directions, and the structure laid down here — concepts as types, modalities as adjoints, essences as propositions — is meant to make those extensions natural rather than forced.

Cubical primitives reference

Reference, not tutorial. Skip this page on first read. Each chapter introduces the cubical-Agda constructs it needs in context and links back here for a one-page reminder. Use this appendix when you want the formal definition of _≡_, PathP, Σ, HITs, the unit interval, eta-equality, or absurd patterns — not as a prerequisite tutorial.

This page collects the Cubical Agda machinery used throughout the book in one place. Every chapter links here on first use.

The interval I

Cubical Agda has a primitive type I — the “unit interval.” Its inhabitants are i0 (left endpoint) and i1 (right endpoint), plus a continuous family of points in between. You don’t construct elements of I directly; you receive them as the bound variable of a path (see below).

Paths and _≡_

In plain Agda, equality x ≡ y is a static proposition. In Cubical Agda, x ≡ y is a path between x and y — specifically, a function I → A whose value at i0 is x and at i1 is y.

You construct a path with lambda over I:

constant-path : {A : Set} (x : A) → x ≡ x
constant-path x = λ i → x

The constant path λ i → x always evaluates to x for every i, so it witnesses x ≡ x. This is the reflexivity path, also written refl.

example-refl : {A : Set} (x : A) → x ≡ x
example-refl x = refl

refl and λ i → x are interchangeable.

PathP (dependent paths)

PathP is the dependent version of _≡_: a path in a family of types that varies along the interval. You won’t construct PathP directly very often, but you’ll see it in type signatures generated by Agda when paths cross type boundaries. For the purposes of this book, treat PathP (λ _ → A) x y as identical to x ≡ y.

Dependent pairs: Σ, _,_, fst, snd

The cubical library re-exports the builtin dependent pair type:

-- Σ has signature
Σ : (A : Set) → (A → Set) → Set

-- with constructor _,_
example : Σ ⊤ (λ _ → ⊤)
example = (tt , tt)

For non-dependent pairs we often define a separate _×_ record (as in Chapter 3) because it has nicer pattern-matching.

Absurd patterns

When a function takes an argument of type ⊥ (the empty type), there is nothing to define — ⊥ has no inhabitants, so the function is “defined” vacuously. Agda’s syntax for this is the absurd pattern ():

from-nothing : {X : Set} → ⊥ → X
from-nothing ()

The body of the function is omitted; the () tells the typechecker that no case is missing.

Eta-equality for records

A record type with one constructor and explicit fields enjoys eta-equality: any value of the record is judgmentally equal to the constructor applied to its projections. Concretely, for the unit type:

record ⊤ : Set where
  constructor tt

any x : ⊤ is judgmentally equal to tt. So λ i → tt is a path from tt to any y : ⊤ — because y is tt.

Higher Inductive Types (HITs)

Standard Agda lets you define types with point constructors:

data Bool : Set where
  true  : Bool
  false : Bool

Cubical Agda lets you also define path constructors:

data Becoming : Set where
  being   : Becoming
  nothing : Becoming
  werden  : being ≡ nothing

werden adds a path identifying being with nothing. This is a Higher Inductive Type — “higher” because it lives at a higher homotopical level than ordinary inductive types.

We use this in Chapter 4 to model Hegel’s claim that Sein ≡ Nichts.

The libraries

The book imports from the agda/cubical library. CI uses version 0.8 (paired with Agda 2.7.0.1); version 0.9 (paired with Agda 2.8.0) also works locally. The key modules are:

• Cubical.Core.Primitives — I, _≡_, PathP, Σ, _,_
• Cubical.Foundations.Prelude — refl, sym, _∙_, cong, transport

You shouldn’t need to import other cubical modules to follow this book.

Glossary

Hegelian terms first (alphabetised by German), then Agda terms.

Hegelian terms

Aufhebung (sublation)

Hegel’s term for the resolution of a dialectical contradiction into a higher concept that “cancels, preserves, and elevates” the moments of the lower one. Combines three German senses (aufheben can mean “lift up,” “abolish,” or “preserve”).

Introduced in Chapter 4.

Begriff (Concept)

Hegel’s most fundamental unit. In the Doctrine of the Notion the Concept is treated as a self-developing unity of universality, particularity, and individuality. We capture only the static “container” reading in this book.

Introduced in Chapter 1.

Dasein (Determinate Being)

The first concept after Pure Being and Pure Nothing have been sublated through Becoming. Hegel’s term for being-with-determination.

Discussed in Chapter 3.

Möglichkeit (Possibility)

In Hegel’s discussion of Actuality (§1191), one of three modal moments. The Lawvere reading identifies Possibility with the dependent sum Σ.

Introduced in Chapter 6.

Nichts (Pure Nothing)

The categorical opposite of Pure Being. Hegel insists Pure Nothing has the same indeterminacy as Pure Being — both lack any qualities — which sets up the dialectical move to Becoming. Modeled as the empty type ⊥.

Introduced in Chapter 2.

Notwendigkeit (Necessity)

The third modal moment in Hegel’s discussion of Actuality. The Lawvere reading identifies Necessity with the dependent product Π.

Introduced in Chapter 6.

Reflexion (Reflection)

In the Doctrine of Essence, the act of a concept appearing within the universe of essential truths. We capture one fragment of this as a characteristic map X → Ω.

Introduced in Chapter 5.

Schein (Illusory being, Appearance)

The surface appearance of a concept, distinct from its Essence (Wesen). Hegel’s Doctrine of Essence opens with the distinction of Essence from Appearance.

Discussed in Chapter 5.

Schluss (Syllogism)

The connection of two Judgments through a mediating middle term. The classical form is the Aristotelian “All B are A; E is B; therefore E is A.” We model it by function composition.

Introduced in Chapter 1.

Sein (Pure Being)

The most abstract concept — pure existence without further qualities. The absolute starting point of the Science of Logic. Modeled as the unit type ⊤.

Introduced in Chapter 2.

Urteil (Judgment)

The assertion that an individual belongs to a Concept. Literally “primal division” — Ur-Teil. We model it as the typing judgment c : C.

Introduced in Chapter 1.

Werden (Becoming)

The unity of Pure Being and Pure Nothing. Hegel’s first dialectical result: Sein and Nichts pass over into each other, and their truth is the movement between them. Modeled in Chapter 2 by the bare arrows ⊥ → X → ⊤, and in Chapter 4 more strongly by a Higher Inductive Type with an explicit path between Being and Nothing.

Wesen (Essence)

The subject of Hegel’s second book (Doctrine of Essence). What survives when mere Appearance is set aside. We model fragments of Wesen using the type Ω of mere propositions.

Introduced in Chapter 5.

Wirklichkeit (Actuality)

The subject of Hegel’s discussion of modality (§1191). Truth placed in a concrete context. The Lawvere reading identifies Actuality with type-theoretic weakening (a value lifted into a context).

Introduced in Chapter 6.

Agda terms

⊤ (top, unit type)

A type with exactly one inhabitant tt. Used to model Pure Being.

record ⊤ : Set where
  constructor tt

⊥ (bottom, empty type)

A type with no inhabitants. Used to model Pure Nothing.

data ⊥ : Set where

_≡_ (path equality)

In Cubical Agda, x ≡ y is a path between x and y. See the Cubical primitives reference.

refl

The reflexivity path x ≡ x. Identical to λ i → x.

Σ (dependent sum)

The type of pairs (a, b) where a : A and b : B a. Used to model Possibility (Chapter 6).

Π (dependent product)

The dependent function type (a : A) → B a. Used to model Necessity (Chapter 6).

Set

Agda’s universe of types. Despite the name, Set does not refer to set-theoretic sets — it just means “type.” The naming is historical.

Set₁

The universe of types-of-types. Set : Set₁. Types containing universe-level things live one level up.

isContr A

A type expressing that A is contractible — has a center point connected by paths to every inhabitant. Strictly stronger than “A has one element.”

isProp A

A type expressing that A is a proposition — any two inhabitants are path-equal. The proposition-level fragment of Essence in Chapter 5.

Ω

The type of all propositions. Introduced in Chapter 5 as the classifier of essential truths.

postulate

Agda’s keyword for “assume this exists without construction.” Used sparingly in this book for abstract starting points; later chapters drop postulates in favor of real proofs.

Higher Inductive Type (HIT)

A type definition that includes path constructors as well as point constructors. Used in Chapter 4 to model Sein ≡ Nichts.

Absurd pattern ()

Used as the body of a function whose input type is empty. Tells Agda there is no case to handle.

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.