Reference Sheet 2: Homotopy Type Theory for Identity and Equivalence#

Target audience: Forge auditor who knows S5 modal logic, CEM, FOL, and basic game theory but needs HoTT for formalizing identity, equivalence, and version relationships between model variants.

1. Orientation#

Homotopy Type Theory (HoTT) is a foundation of mathematics where equality is not a mere predicate but a structure. In classical logic, two things are either equal or not — period. In HoTT, there can be multiple distinct ways in which two things are the same, and these ways themselves can be compared. This directly addresses the matheology system’s core versioning question: when model version PPv1r1p1 and OOv2r0p0 both formalize “God contains the world,” are they “the same” axiom? HoTT says: tell me the path between them, and I will tell you how same they are. The VVN system tracks versions; HoTT gives versions a rigorous mathematical semantics.

2. Key Concepts#

Type. In HoTT, everything is a type. A proposition is a type (its elements are proofs). A set is a type (its elements are members). A space is a type (its elements are points). Notation: a : A means “a is of type A.” Contrast with FOL where terms, formulas, and sets are distinct syntactic categories. Matheology use: “PET-model” is a type. Each specific version (iv_LLoL_PPv1r1p1_2026m03d14) is an element of that type. The type itself captures what all versions share.

Path type (identity type). For a,b : A, the type a =_A b (or Path_A(a,b)) is the type of evidence that a and b are the same. A path p : a =_A b is a specific proof of sameness. There can be zero paths (a ≠ b), one path (unique sameness), or many paths (structurally different proofs of sameness). Matheology use: Two VVN versions of an axiom may have multiple distinct equivalence proofs — one via syntactic rewriting, another via semantic model-checking. These are different paths, and their distinctness is mathematically meaningful.

Path composition and inversion. Paths compose: if p : a = b and q : b = c, then q ∘ p : a = c. Paths invert: if p : a = b, then p⁻¹ : b = a. With reflexivity refl_a : a = a, paths form a groupoid structure. Matheology use: If version V1 is equivalent to V2 (path p) and V2 to V3 (path q), then V1 is equivalent to V3 via q ∘ p. The revision history is a groupoid, not just a linear chain.

Transport. Given a type family P : A → Type and a path p : a =_A b, transport gives a function transport(P, p) : P(a) → P(b). Informally: a proof about a can be “carried along the path” to become a proof about b, provided you specify which type family you are transporting along. Matheology use: If axiom ax5 in PPv1 is path-equivalent to ax5 in OOv2, then a theorem proved from PPv1’s ax5 can be transported to a theorem in OOv2’s context. Transport makes version migration rigorous.

Univalence axiom. (A ≃ B) ≃ (A =_U B) — equivalence of types is equivalent to identity of types in the universe U. Informally: if two structures are equivalent (there is a structure-preserving bijection between them), then they are the same type, and you can substitute one for the other in any context. Matheology use: If PET-PPv1 and PET-OOv2 are equivalent as formal systems (same theorems, same proof structure up to isomorphism), then univalence says they are the same model and all results transfer freely. This is stronger than “they happen to prove the same things.”

Higher inductive type (HIT). A type defined not only by its constructors (how to build elements) but also by its path constructors (what equalities hold between elements). Example: the circle S¹ has one point constructor (base) and one path constructor (loop : base = base). Matheology use: A model version type could be defined as a HIT: the constructors are the version releases, and the path constructors are the formally checked equivalence proofs between versions. The resulting type automatically inherits the groupoid structure of version equivalences.

Truncation levels (h-levels).

  • h-level −2: contractible (one element, unique)

  • h-level −1: proposition (at most one element — truth value)

  • h-level 0: set (elements are discrete — paths are unique if they exist)

  • h-level 1: groupoid (paths between elements may be non-trivially different)

Matheology use: Are axiom identities propositional (two versions are either equivalent or not, no further structure) or groupoidal (there are meaningfully different ways they can be equivalent)? The answer determines which HoTT machinery is needed.

Fiber and fibration. For f : A → B and b : B, the fiber of f over b is the type Σ(a : A), f(a) = b — all elements of A that map to b, together with the proof. A fibration is a type family that varies continuously over a base type. Matheology use: The axioms that entail a given theorem form the fiber of the “entailment map” over that theorem. Different fibers may have different sizes and structures — some theorems have unique proofs, others have multiple independent proof paths.

3. Critical Theorems#

Univalence implies function extensionality. If two functions agree on all inputs (∀x, f(x) = g(x)), then f = g as functions. This is not provable in plain Martin-Löf type theory but follows from univalence. Why it matters: Two model compilers that produce identical output for all inputs are the same compiler. Without function extensionality, you cannot prove this — you can only observe it case by case. With univalence, structural equivalence of compilers is a theorem.

The encode-decode method. A general technique for characterizing path types: to understand a =_A b, define a “code” type Code(a,b) that you can compute with, and show Code(a,b) ≃ (a = b). This reduces identity questions to concrete computation. Why it matters: When asking “is VVN version X the same as version Y?”, the encode-decode method gives a recipe: define what “sameness evidence” looks like concretely (e.g., a list of axiom-by-axiom equivalence proofs), then show this concrete evidence type is equivalent to the abstract path type.

Structure Identity Principle (SIP). For structured types (groups, rings, models), the identity type between two structures is equivalent to the type of structure-preserving isomorphisms between them. This is a consequence of univalence. Why it matters: Two matheology models are identical-as-types if and only if there is a structure-preserving isomorphism between them. SIP makes this precise: you do not need to compare axioms one-by-one; you need a single isomorphism that respects derivability.

Whitehead’s theorem for n-types. A map between n-types that induces isomorphisms on all homotopy groups is an equivalence. Informally: for truncated types, local equivalence implies global equivalence. Why it matters: If two model versions agree on all “levels” of structure (axioms, theorems, meta-theorems), then they are equivalent as types. You do not need to check infinite-dimensional structure for finitely-truncated mathematical models.

4. Common Pitfalls#

Treating paths as propositions. In classical logic, a = b is either true or false. In HoTT, a =_A b is a type that can have zero, one, or many inhabitants. If you reason as though equality is propositional when it is not, you will silently drop equivalence data. Always check the h-level before assuming uniqueness of paths.

Confusing equivalence (≃) with equality (=). Before univalence, equivalence and equality are different. Equivalence is a structure (a function with contractible fibers). Equality is a path. Univalence bridges them, but only in a universe. Inside a fixed type, equivalence of elements is not equality of elements — it is a path between them.

Forgetting to specify the type family in transport. Transport requires a type family P. The same path p : a = b produces different transported results depending on which P you choose. In matheology terms: the “same” version equivalence proof carries different theorems to different conclusions depending on which aspect of the model you are transporting.

Assuming all types are sets. Many mathematical objects are naturally groupoids or higher. If you truncate to h-level 0 (sets) by default, you lose information about distinct proof paths. For the VVN system, this means losing the distinction between “these versions are equivalent by syntactic rewriting” and “these versions are equivalent by deep structural isomorphism.”

Over-applying univalence. Univalence applies between types in a universe, not between elements of a fixed type. You cannot use univalence to prove 3 = 5 just because there is a bijection between {0,1,2} and {0,1,2}. Keep clear which level of structure you are reasoning about.

5. Bridge to Matheology#

VVN versions as a higher inductive type. Define the type PET-Versions with:

  • Point constructors: one for each released version (PPv1r0p0, PPv1r1p0, PPv1r1p1, …)

  • Path constructors: one for each formally checked equivalence between versions

  • Higher path constructors (if needed): proofs that two equivalence proofs are themselves “the same” or “different”

This type automatically encodes the full version-equivalence structure. The VVN naming convention is a presentation of this HIT.

Model identity via Structure Identity Principle. Question: “Are PET and JUB the same model in different notation, or genuinely different models?” SIP answers: they are the same if and only if there is a derivability-preserving isomorphism between them. Since JUB has axioms with no PET counterpart (ax15–ax25 extend, not restate), no such isomorphism exists — JUB is genuinely an extension, not a reformulation. This is now a theorem, not an intuition.

Transport for version migration. When upgrading from OOv1 to OOv2, theorems proved in OOv1 can be transported to OOv2 if you can exhibit a path (equivalence proof) between the relevant axiom versions. Transport tells you exactly which theorems survive the migration and which ones need re-proving because the path does not exist for their specific axiom dependencies.

HELL findings and path structure. A HELL con-finding that attacks theorem T is, in HoTT terms, evidence that a claimed path does not exist — the theorem does not follow from the axioms via the claimed route. A pro-finding is a repair: a new path (possibly via a different route) that restores the derivation. Tracking these as paths rather than booleans preserves the information about which proof strategy succeeded.

New questions HoTT enables:

  • What is the h-level of the PET model type? If it is a set (h-level 0), then version equivalences are unique when they exist. If it is a groupoid (h-level 1), there are meaningfully different ways for versions to be equivalent.

  • Can the 5D label space (BEST naming) be formalized as a fibration, with the compiled output varying continuously over the label base space?

  • Does the PET → JUB extension have a section — a way to embed JUB-specific results back into the PET context without loss?