Part V

Category Theory and Homotopy Type Theory: Composition and Identity

math.CT · 24 pages

Abstract

This is Part V of a seven-part modular series that formalizes each mathematical domain as a physical-representation module. Parts I–IV built a representation stack: mathematical structures $M$ are sent by an abstraction map $Φ$ to abstract physical-information objects, realized by a channel $Real_{α}$ into physical representations, and read off by an observation map $Obs$ , giving the master pipeline $Obs_{α} (M) = Obs (Real_{α} (Φ (M)))$ . Those modules used functoriality (topological quantum field theory as a functor $Bord_{n} \to Vect$ ; realization channels as translations between worlds) without isolating the grammar that makes such translation coherent. The present module supplies that grammar. We treat category theory as the theory of composition and identity: the associativity and unit laws that let physical processes be chained, and functors and natural transformations as the structure-preserving translations and their uniform deformations. We then treat homotopy type theory (HoTT) as the theory of identity proper: identity types as paths, path induction as the sole generator of transport, and Voevodsky’s univalence axiom as the principle that equivalent representations are identified rather than merely related. Four theorems anchor the module. (T1) Univalence turns Part I’s Axiom (Equivalence) from a postulate into a theorem for every internally definable realization. (T2) The Curry–Howard–Lambek correspondence exhibits a single composite functor $TypeTheory \to C \to Phys$ interpreting logic, code, and physical representation at once. (T3) In a dagger-compact category the existence of uniform natural copying forces cartesianness, giving a structural no-cloning theorem that explains why Part VI’s quantum high-availability encodings must be genuine embeddings rather than replications. (T4) The groupoid (higher) quotient $X / / G$ is strictly finer than the set quotient $X / G$ , reconstructing the “stacks retain gauge information” phenomenon inside the truncation hierarchy of HoTT and setting up Part VI’s stacks. Throughout we preserve the S/H/P epistemic status discipline of the series, provide runnable Haskell encodings of the category/functor/composition structures, and sketch an idiomatic Lean formalization. Category theory and HoTT are thus the compositional glue of the whole library: they are the module in which the laws of composition and identity that bind Parts I–VI are made explicit.

1 Introduction

1.1 Where this module sits

The series A Math $\to$ Physics Representation Library formalizes the thesis that many physical quantities are not merely described by mathematics but are obtained as realizations of structured mathematical information. The organizing device is a representation stack together with a realization pipeline

M \in Math_{d} Φ abstract information Φ (M) Real_{α} physical representation Obs measurement data, (1)

compressed into the universal formula

Obs_{α} (M) = Obs (Real_{α} (Φ (M))) i.e. observable = Real (abstract structure) . (2)

Each entry of the library carries an epistemic status label

σ \in {S, H, P}

: S (standard mathematics or mathematical physics), H (strong heuristic dictionary entry), P (speculative ontological extension); composite labels

S/H

and

H/P

denote entries that are standard as mathematics but heuristic or speculative in their physical reading. This labelling is part of the formalism, not decoration, and we apply it verbatim throughout.

The modular ladder is $stack I \to motives II \to geometry III \to topology IV \to category theory & HoTT V \to stacks, gauge, quantum HA VI \to Synthesis .$ Part IV exhibited one rigorous instance of “physics as a functor”: a topological quantum field theory (TQFT) is a symmetric monoidal functor $Z : Bord_{n} \to C$ [10, 6]. But Part IV used the word “functor” without developing the general theory of functors, and it used “equivalent realizations describe the same physics” without a formal notion of identity of structures. Part V is exactly the abstraction step that provides both:

category theory is the grammar of physical composition;
HoTT is the logic of spaces, paths, equivalences, and higher identity.

Because every realization channel $Real_{α}$ , every duality, and every symmetry of Parts I–IV is a morphism, functor, or equivalence, Part V is the compositional glue of the whole library: it is where the laws of composition and identity that bind Parts I–VI are isolated and proved. It also sets up Part VI, whose stacks are groupoid-valued sheaves built from the categorical and truncation machinery introduced here.

1.2 Contributions

A categorical recasting of the realization pipeline (2). We show that (1) is literally a composite of functors between the groupoids of a representation prestack, so that the associativity and unit laws of the library are the associativity and unit laws of a category (4). This turns Part I’s informal “composition of compatible translations” into a theorem.
The composition/identity core (3, 4). We give precise definitions of categories, functors, natural transformations, functor categories, and monoidal and dagger-compact structure, with the interchange law and an Eckmann–Hilton argument (13) that already exhibits the interaction of two compositions with a shared identity—the thematic centre of the module.
Univalence discharges the Equivalence axiom (27, T1). We prove that any internally definable realization respects equivalence of structures, so Part I’s Axiom (Equivalence) becomes a theorem in a univalent model.
A single functor for logic, code, and physics (29, T2). The Curry–Howard–Lambek correspondence yields a composite functor $TypeTheory \to C \to Phys$ interpreting the three-way dictionary (proof $=$ program $=$ physical realization) as one categorical translation.
A structural no-cloning theorem (31, T3). In a dagger-compact category, uniform natural copying forces the monoidal product to be a categorical product; since the tensor product of finite-dimensional Hilbert spaces is not a product, quantum high availability (Part VI) is representationally forced to be encoding, not replication.
Groupoid quotients are finer than set quotients (33, T4). We reconstruct “stacks retain gauge information” purely inside the HoTT truncation hierarchy: $X / / G$ is a $1$ -type retaining stabilizer loops, while $X / G$ is its $0$ -truncation, forgetting them.
Formal artifacts. A runnable Haskell package encoding categories, functors, natural transformations, dagger-compact structure, and groupoid-vs-set quotients (8), and an idiomatic Lean sketch of the category/functor/identity-law types (9).

1.3 Epistemic status and limitations

We reproduce the series-wide limitations in the form relevant to this module. Category theory and HoTT are status S mathematics; their status becomes $S/H$ or $H$ only when we read a specific categorical or type-theoretic construction as a claim about physics. In particular: (i) we do not claim a single universal functor $Math \to Phys$ —the representation approach is deliberately domain-indexed (2); (ii) reading a type $A$ as a “space of physical possibilities” is a heuristic semantic layer (status $H$ ), flagged as such; (iii) univalence is a theorem-generating principle about mathematical structures, and its physical reading (“equivalent representations are the same physical content”) is $S/H$ . These flags are carried explicitly in the dictionary of 7 and 12.

1.4 Outline

2 recalls the representation-stack framework and casts the pipeline categorically. 3 develops categories, functors, natural transformations, and the interchange/Eckmann–Hilton phenomena. 4 develops monoidal, symmetric, compact-closed and dagger-compact structure and string diagrams. 5 develops HoTT: identity types, path induction, transport, equivalence, and univalence. 6 proves the four theorems T1–T4. 7 presents the category-theory/HoTT representation dictionary with S/H/P labels. 8, 9 give the Haskell and Lean formalizations. 10 discusses composition in the ladder and limitations; 11 concludes. 12 contains the full dictionary longtables.

2 Mathematical framework: the representation stack, categorically

We recall the minimum from Part I and immediately reorganize it so that the categorical language of 3 applies.

Definition 1 (Representation entry, Part I). A representation entry is a quadruple $E = (M, P, τ, σ)$ where $M \in Math_{d}$ is a mathematical structure in a domain $d \in Dom$ , $P \in Phys$ is a proposed physical representation, $τ$ is a semantic translation datum (a functor, a natural transformation, an equivalence class of models, or a weaker interpretation map), and $σ \in {S, H, P}$ is the epistemic status label.

Definition 2 (Representation prestack, Part I). A representation prestack is a pseudofunctor $Rep_{Phys} : Dom^{op} \to Grpd$ assigning to each domain $d$ a groupoid $Rep_{Phys} (d)$ of representation entries, and to a domain refinement $u : e \to d$ a restriction functor $u^{*} : Rep_{Phys} (d) \to Rep_{Phys} (e)$ , functorial up to coherent natural isomorphism.

The words “groupoid”, “functor”, “natural isomorphism”, and “pseudofunctor” in 2 are precisely the notions 3 makes rigorous; Part I used them on trust. We keep the realization pipeline (1) but now name its stages as morphisms in categories.

Definition 3 (Realization data). Fix a domain $d$ . A realization datum of level $α$ consists of: an abstraction functor $Φ : Math_{d} \to A$ into a category $A$ of abstract physical-information objects; a realization functor $Real_{α} : A \to Phys$ ; and an observation functor $Obs : Phys \to M$ into a category $M$ of measurement data. The pipeline of level $α$ is the composite functor $Obs_{α} := Obs \circ Real_{α} \circ Φ : Math_{d} ⟶ M .$

Theorem 4 (The pipeline is a composite of functors). With the data of 3, $Obs_{α}$ is a functor, and its formation is associative and unital: for composable domain refinements the restriction functors compose (up to coherent isomorphism), and the identity refinement acts as the identity functor. Consequently the master formula (2) is the object-level shadow of a genuine composition of morphisms in $Cat$ , and Part I’s closure operation “composition of compatible translations” is the composition law of the category $Cat$ of categories.

Proof. Functors compose: if $F : X \to Y$ and $G : Y \to Z$ preserve identities and composition, then $(G \circ F) (id_{X}) = G (id_{F X}) = id_{GF X}$ and $(G \circ F) (g \circ f) = G (F g \circ F f) = G (F g) \circ G (F f)$ , so $G \circ F$ is a functor. Applying this twice to $Φ$ , $Real_{α}$ , $Obs$ gives that $Obs_{α}$ is a functor. Associativity of $\circ$ in $Cat$ is inherited from associativity of function composition on objects and on hom-sets; the identity functor $id_{X}$ is a two-sided unit for the same reason. The pseudofunctoriality clause of 2 states exactly that $u^{*} \circ v^{*} ≅ (v \circ u)^{*}$ and $(id_{d})^{*} ≅ id$ , which is associativity and unitality up to coherent isomorphism. Reading (2) on objects, $Obs_{α} (M) = Obs (Real_{α} (Φ (M)))$ is the value of the composite functor at $M$ , i.e. the object component of the composition $Obs \circ Real_{α} \circ Φ$ in $Cat$ . ◻

4 is the reason category theory belongs at Level V of the ladder: the entire library was already, implicitly, a diagram in $Cat$ . The remaining sections make the ingredients precise and extract the four physical consequences T1–T4. The pipeline as a commuting diagram is:

Math_{d}

A

Phys

M

$Math_{d}$ → $A$ $Φ$
$Math_{d}$ → $M$ $Obs_{α}$
$A$ → $Phys$ $Real_{α}$
$Phys$ → $M$ $Obs$

3 Categories, functors, and natural transformations

3.1 Categories: composition and identity

Definition 5 (Category). A category $C$ consists of a collection $Ob (C)$ of objects; for each ordered pair $(A, B)$ a set $Hom_{C} (A, B)$ of morphisms; a composition operation $\circ : Hom (B, C) \times Hom (A, B) \to Hom (A, C)$ ; and for each object $A$ an identity morphism $id_{A} \in Hom (A, A)$ , subject to the two axioms

(associativity) (unit) h \circ (g \circ f) = (h \circ g) \circ f, id_{B} \circ f = f = f \circ id_{A} for f : A \to B . (3-4)

Physically (status $S/H$ ), objects are systems or state spaces, morphisms $f : A \to B$ are processes or transitions, $g \circ f$ is “do $f$ , then $g$ ”, and $id_{A}$ is the do-nothing process. (3) says that grouping of a process chain is physically immaterial; (4) says that inserting a trivial step changes nothing. These two laws are the entire content of “composition and identity” at the $1$ -categorical level.

Example 6 (Groups and representations as one-object categories). A monoid $M$ is a category with one object $*$ and $Hom (*, *) = M$ , with composition the monoid product and identity the unit. A group $G$ is such a category in which every morphism is invertible—a one-object groupoid, written $B G$ (the delooping). A linear representation $ρ : G \to G L (V)$ is exactly a functor $B G \to Vect$ : it sends the unique object to $V$ and each group element to an invertible linear map, and functoriality $ρ (g h) = ρ (g) ρ (h)$ , $ρ (e) = id_{V}$ is the definition of a representation. This is the first place the slogan “a physical theory is a functor” becomes literal: a symmetry action is a functor out of a delooping.

Example 7 (Preorders, spaces, and $FdHilb$ ). (i) A preorder $(P, \leq)$ is a category with at most one morphism $A \to B$ , present iff $A \leq B$ ; composition is transitivity, identities are reflexivity. (ii) $Set$ has sets as objects and functions as morphisms; $Vect$ has vector spaces and linear maps; $FdHilb$ has finite-dimensional Hilbert spaces and linear maps. (iii) The bordism category $Bord_{n}$ has closed $(n - 1)$ -manifolds as objects and $n$ -dimensional cobordisms (up to diffeomorphism) as morphisms; a TQFT is a functor $Bord_{n} \to Vect$ (7 feeds 4).

Definition 8 (Isomorphism, groupoid). A morphism $f : A \to B$ is an isomorphism if there is $g : B \to A$ with $g \circ f = id_{A}$ and $f \circ g = id_{B}$ ; then $g$ is unique and written $f^{- 1}$ . A groupoid is a category in which every morphism is an isomorphism. Physically (status $S$ ) an isomorphism is a reversible equivalence: “the same structure in different coordinates.”

3.2 Functors: translation between worlds

Definition 9 (Functor). A functor $F : C \to D$ assigns to each object $A$ an object $F A$ and to each morphism $f : A \to B$ a morphism $F f : F A \to F B$ , preserving identities and composition:

F (id_{A}) = id_{F A}, F (g \circ f) = F g \circ F f . (5)

A functor is the structure-preserving translation of the composition/identity laws from one world to another; a physical theory, a quantization, or a realization channel $Real_{α}$ is such a translation (status $S$ for TQFT; $S/H$ for a general realization functor). (5) is precisely what makes pipeline cd commute stagewise.

Definition 10 (Natural transformation). Given functors $F, G : C \to D$ , a natural transformation $η : F \Rightarrow G$ is a family of morphisms $η_{A} : F A \to G A$ (its components) such that for every $f : A \to B$ the naturality square commutes:

F A

G A

F B

GB

$F A$ → $G A$ $η_{A}$
$F A$ ↓ $F B$ $F f$
$G A$ ↓ $GB$ $G f$
$F B$ → $GB$ $η_{B}$

⟺ G f \circ η_{A} = η_{B} \circ F f .

If each

η_{A}

is an isomorphism,

η

is a natural isomorphism and

F ≅ G

. Physically (status

S/H

) a natural transformation is a uniform deformation of one translation into another—a field redefinition or theory equivalence that acts coherently on all systems at once.

Definition 11 (Functor category). For categories $C, D$ , the functor category $[C, D]$ has functors $C \to D$ as objects and natural transformations as morphisms, with vertical composition $(θ \cdot η)_{A} = θ_{A} \circ η_{A}$ and identity the identity natural transformation. There is also horizontal composition $*$ of natural transformations along a composite of functors.

3.3 Interchange and Eckmann–Hilton

In the functor $2$ -category $Cat$ , objects are categories, $1$ -morphisms are functors, and $2$ -morphisms are natural transformations. These $2$ -morphisms carry two composition laws. Their compatibility is the single most important coherence in the module, because “composition and identity” now appears twice—two compositions sharing one family of identities.

Proposition 12 (Interchange law). In any $2$ -category, for $2$ -morphisms arranged so that both sides are defined,

(θ^{'} \cdot θ) * (η^{'} \cdot η) = (θ^{'} * η^{'}) \cdot (θ * η), (6)

where $\cdot$ is vertical and $*$ is horizontal composition. In particular horizontal and vertical composition of natural transformations satisfy (6).

Proof. Both sides are computed by evaluating components and using naturality naturality. Writing the horizontal composite of $η : F \Rightarrow G$ (along $C \to D$ ) with $η^{'} : F^{'} \Rightarrow G^{'}$ (along $D \to E$ ) as $(η^{'} * η)_{A} = η_{G A}^{'} \circ F^{'} η_{A} = G^{'} η_{A} \circ η_{F A}^{'}$ (the two expressions agree by naturality of $η^{'}$ at $η_{A}$ ), one expands both sides of (6) on an object $A$ and finds each equal to the common diagonal of the evident commuting square; the equality is forced by the naturality of the four transformations. A full component computation is standard [1]. ◻

Proposition 13 (Eckmann–Hilton). Let a set $S$ carry two unital binary operations $\cdot$ and $*$ sharing a common unit $e$ and satisfying the interchange law $(a * b) \cdot (c * d) = (a \cdot c) * (b \cdot d)$ . Then the two operations coincide, are associative, and are commutative.

Proof. First $e = e * e = e \cdot e$ . Interchange gives, for all $a, b$ , $a * b = (a \cdot e) * (e \cdot b) = (a * e) \cdot (e * b) = a \cdot b,$ so $* = \cdot$ ; call it $\times$ . Then $a \times b = (e * a) \times (b * e) = (e \times b) * (a \times e) = b \times a$ , giving commutativity, and interchange collapses to associativity. ◻

Remark 14 (Why this belongs to a module titled “composition and identity”). 13 is the algebraic reason that the second homotopy group of a space is abelian, and in HoTT it is the statement that the higher identity types $Ω^{2}$ (paths between paths) are commutative: the two ways to compose $2$ -dimensional identities—horizontally and vertically—share the constant identity and interchange, hence agree and commute. Thus “composition” and “identity” are not two topics but one: at each new dimension the identity laws constrain how compositions may interact, and Eckmann–Hilton is the first nontrivial constraint. This directly forecasts the higher-identity content of 5.

3.4 Yoneda: a system is known by its probes

Lemma 15 (Yoneda). For a locally small category $C$ , an object $A \in C$ , and a functor $F : C^{op} \to Set$ , there is a bijection natural in both $A$ and $F$ ,

Nat (Hom_{C} (-, A), F) ≅ F (A), η \mapsto η_{A} (id_{A}) . (7)

In particular the Yoneda embedding $y : C ↪ [C^{op}, Set]$ , $A \mapsto Hom_{C} (-, A)$ , is full and faithful, so $A ≅ B$ iff $Hom (-, A) ≅ Hom (-, B)$ .

Proof. Given a natural transformation $η : Hom (-, A) \Rightarrow F$ , set $u := η_{A} (id_{A}) \in F (A)$ . Naturality at any $f : X \to A$ (viewed as an element of $Hom (X, A)$ ) forces $η_{X} (f) = F (f) (u)$ , so $η$ is determined by $u$ ; and any $u \in F (A)$ defines a natural $η$ by this formula. The two assignments are mutually inverse, giving (7). Naturality in $A, F$ is a direct check. Taking $F = Hom (-, B)$ yields $Nat (Hom (-, A), Hom (-, B)) ≅ Hom (A, B)$ , i.e. full faithfulness of $y$ ; reflection of isomorphisms follows because full and faithful functors reflect isomorphisms. ◻

Physically (status $S/H$ ) the Yoneda lemma is the statement that a system is completely determined by the totality of its responses to all probes: knowing $Hom (-, A)$ —all ways of mapping into $A$ —determines $A$ up to isomorphism. This is the categorical form of an operational/measurement-based identity criterion and reappears as the “univalence for representables” motif in 5.

4 Monoidal and dagger-compact structure

Parallel composition of systems—putting two experiments side by side—is not captured by $\circ$ alone. It is captured by a tensor product, and the reversal of processes by a dagger. These structures make $FdHilb$ into the ambient category of finite quantum mechanics and give the string-diagram calculus used in Part VI.

Definition 16 (Monoidal category). A monoidal category is a category $C$ with a functor $\otimes : C \times C \to C$ , a unit object $I$ , and natural isomorphisms $α_{A, B, C} : (A \otimes B) \otimes C \to A \otimes (B \otimes C)$ , $λ_{A} : I \otimes A \to A$ , $ρ_{A} : A \otimes I \to A$ satisfying Mac Lane’s pentagon and triangle coherence axioms. It is symmetric if it also has a natural isomorphism $σ_{A, B} : A \otimes B \to B \otimes A$ with $σ_{B, A} \circ σ_{A, B} = id$ and the hexagon coherence.

That $\otimes$ is a bifunctor means it respects composition in each argument and satisfies the interchange law $(g \otimes g^{'}) \circ (f \otimes f^{'}) = (g \circ f) \otimes (g^{'} \circ f^{'})$ : sequential and parallel composition of processes commute, which is the algebra of quantum circuits. Physically (status $S$ ) $A \otimes B$ is the composite system, $I$ is the trivial system, and $σ$ is the swap—bosonic-like exchange when it squares to the identity, anyonic braiding when it does not.

Definition 17 (Compact closed and dagger-compact category). A compact closed category is a symmetric monoidal category in which every object $A$ has a dual $A^{*}$ equipped with a unit $η_{A} : I \to A^{*} \otimes A$ (coevaluation, a “cup”) and counit $ε_{A} : A \otimes A^{*} \to I$ (evaluation, a “cap”) satisfying the snake (zig-zag) equations

(ε_{A} \otimes id_{A}) \circ (id_{A} \otimes η_{A}) = id_{A}, (id_{A^{*}} \otimes ε_{A}) \circ (η_{A} \otimes id_{A^{*}}) = id_{A^{*}} . (8)

A dagger-compact category adds an involutive, identity-on-objects, contravariant functor

(-)^{†}

that is monoidal and compatible with the compact structure, so that

ε_{A} = η_{A}^{†} \circ σ

up to the canonical isomorphisms. Physically

(-)^{†}

is the adjoint/time-reversal.

Example 18 ( $FdHilb$ as the arena of finite quantum mechanics). $FdHilb$ is dagger-compact: $\otimes$ is the tensor product of Hilbert spaces, $I = C$ , $A^{*}$ is the dual space, $η_{A} (1) = \sum_{i} e_{i} \otimes e_{i}$ is the (unnormalized) Bell state, $ε_{A}$ is the pairing, and $(-)^{†}$ is the Hermitian adjoint. The snake equations (8) are the statement that a maximally entangled pair can be created and then partially annihilated to yield an identity wire—the diagrammatic engine of quantum teleportation [4, 3].

The snake equation admits the string-diagram reading in which a cup followed by a cap straightens a bent wire:

A

A \otimes A^{*} \otimes A

A

$A$ → $A \otimes A^{*} \otimes A$ $id_{A} \otimes η_{A}$
$A$ ↘ $A$ $id_{A}$
$A \otimes A^{*} \otimes A$ ↓ $A$ $ε_{A} \otimes id_{A}$

5 Homotopy type theory: identity as path

We now pass from composition (category theory) to identity proper. HoTT is a dependent type theory in which the identity type is interpreted homotopically and Voevodsky’s univalence axiom governs identity of structures.

5.1 Types, terms, and dependent types

We use the judgement $a : A$ (“ $a$ is a term of type $A$ ”). A dependent type $B : A \to U$ (a type family) assigns a type $B (x)$ to each $x : A$ . From it we form the dependent pair and function types

x : A \sum B (x) (total space), x : A \prod B (x) (space of sections) . (9)

Physically (status

S/H

A

is a space of states or possibilities,

a : A

a witnessing state,

B (x)

a fibre of field data over the base point

x

\sum_{x : A} B (x)

the total configuration space, and

\prod_{x : A} B (x)

the space of fields (sections) assigning data at every point.

5.2 Identity types and path induction

Definition 19 (Identity type). For $A : U$ and $a, b : A$ there is a type $Id_{A} (a, b)$ , written $a = b$ , whose terms are identifications (paths) from $a$ to $b$ . It is generated by the constructor $refl_{a} : a = a$ , subject to the following induction principle.

Definition 20 (Path induction, the J-rule). To define a section of a family $C : \prod_{x, y : A} (x = y) \to U$ it suffices to define it on reflexivity: given $c : \prod_{x : A} C (x, x, refl_{x})$ there is a unique (up to identification) term $J (c) : x, y : A \prod p : x = y \prod C (x, y, p) with J (c) (x, x, refl_{x}) \equiv c (x) .$ Path induction is the only elimination rule for identity types.

Lemma 21 (Transport). For any $B : A \to U$ and $p : a = b$ there is an equivalence $transport^{B} (p) : B (a) \sim B (b)$ , with $transport^{B} (refl_{a}) = id_{B (a)}$ , and $transport^{B}$ is functorial: $transport^{B} (q \cdot p) = transport^{B} (q) \circ transport^{B} (p)$ for $p : a = b$ , $q : b = c$ .

Proof. Apply 20 to the family $C (x, y, p) := (B (x) \to B (y))$ with $c (x) := id_{B (x)}$ ; this yields $transport^{B} (p) : B (a) \to B (b)$ with $transport^{B} (refl_{a}) \equiv id$ . That each $transport^{B} (p)$ is an equivalence follows by path induction on $p$ (it holds at $refl$ , hence everywhere), with inverse $transport^{B} (p^{- 1})$ . Functoriality is again path induction: fix $p$ and induct on $q$ ; the case $q = refl_{b}$ reduces to $transport^{B} (p) = transport^{B} (p) \circ id$ , which holds definitionally. ◻

Lemma 22 (Action on paths). Every function $f : A \to B$ acts on identifications: there is $ap_{f} : (a = a^{'}) \to (f (a) = f (a^{'}))$ with $ap_{f} (refl_{a}) = refl_{f (a)}$ , respecting inverses and concatenation. Thus functions automatically preserve identity—the type-theoretic counterpart of functoriality (5).

Proof. Path induction on the family $C (x, y, p) := (f (x) = f (y))$ with $c (x) := refl_{f (x)}$ . Preservation of concatenation and inverses is a further path induction. ◻

5.3 Equivalence and univalence

Definition 23 (Equivalence). A function $f : A \to B$ is an equivalence, written $isEquiv (f)$ , if its fibres are contractible; equivalently if it has a two-sided homotopy-inverse. The type of equivalences is $A ≃ B := \sum_{f : A \to B} isEquiv (f)$ . The canonical map

idtoequiv : (A = B) ⟶ (A ≃ B) (10)

sends

refl_{A}

to the identity equivalence (by path induction).

Definition 24 (Univalence axiom, Voevodsky). A universe $U$ is univalent if for all $A, B : U$ the map $idtoequiv$ of (10) is itself an equivalence:

(A = B) ≃ (A ≃ B) . (11)

Its inverse is written

ua : (A ≃ B) \to (A = B)

Univalence is the exact formal content of the representation-theoretic slogan “equivalent representations can be treated as the same physical content”: identity of structures and equivalence of structures are themselves identified. It is used in 6 to discharge Part I’s Axiom (Equivalence).

Definition 25 (Truncation levels). A type $A$ is contractible (level $- 2$ ) if $\sum_{a : A} \prod_{x : A} (a = x)$ is inhabited; a mere proposition (level $- 1$ ) if all its terms are identified; a set (level $0$ ) if each identity type $a = b$ is a mere proposition; a groupoid (level $1$ ) if each $a = b$ is a set; and so on up the $n$ -truncation hierarchy. Each level $n$ carries an idempotent truncation modality $∥ - ∥_{n}$ universally forcing a type to level $n$ .

Example 26 (The circle). The higher inductive type $S^{1}$ is generated by a point $base : S^{1}$ and a path $loop : base = base$ . It is a $1$ -type, not a set: its loop space is $Ω S^{1} = (base = base) ≃ Z$ , so $π_{1} (S^{1}) = Z$ is provable synthetically. Physically (status $H$ ) $S^{1}$ models a phase circle or winding sector, and its integer loop space is the winding number/topological charge.

6 Results: the four theorems

We now prove the four theorems that give this module its physical payload. T1 and T2 concern identity and translation; T3 and T4 concern quantum information and gauge, feeding Part VI.

6.1 T1: univalence discharges the Equivalence axiom

Theorem 27 (Univalence respects realization). Let $U$ be a univalent universe modelling Part I’s $Math_{d}$ , and let $Real : U \to Phys$ be any internally definable realization, i.e. a function definable in the type theory (equivalently, a term $Real : \prod_{X : U} Phys$ ). Then for all $A, B : U$ , $(A ≃ B) ⟶ (Real (A) = Real (B)),$ and moreover $transport^{Real}$ along the induced path is an equivalence $Real (A) ≃ Real (B)$ . Hence any internally definable realization assigns the same physical representation to equivalent mathematical structures: Part I’s Axiom (Equivalence) is a theorem, not a postulate.

Proof. Let $e : A ≃ B$ . By univalence (11), $ua (e) : A = B$ is an identification of $A$ and $B$ in $U$ . Apply 22 to $Real$ : $ap_{Real} (ua (e)) : Real (A) = Real (B)$ , which is the required identification of physical representations. To obtain an equivalence we transport along the path $ua (e) : A = B$ in the base $U$ , using the type family $X \mapsto Real (X)$ (with $Phys$ read as a universe of types): by 21, $transport^{X \mapsto Real (X)} (ua (e)) : Real (A) \to Real (B)$ is an equivalence, invertible with inverse the transport along $ua (e)^{- 1} = ua (e^{- 1})$ . (Equivalently, applying $idtoequiv$ to the path $ap_{Real} (ua (e))$ in $Phys$ yields the same equivalence directly.) Since $ap_{Real} (refl_{A}) = refl_{Real (A)}$ , the construction sends the identity equivalence to reflexivity, so it is the identity on the diagonal, as required for a bona fide discharge of the axiom. ◻

Remark 28 (Gauge-dependent vs. gauge-invariant). 27 applies only to internally definable realizations. A realization defined by an external choice—picking a basis, a gauge, or a coordinate patch—need not be a term of the type theory and may fail to respect equivalence. This is exactly the physical distinction between gauge-invariant quantities (internally definable; equivalence-respecting) and gauge-dependent quantities (externally defined; not). Univalence thereby draws the gauge-invariance line as a definability condition, anticipating Part VI’s treatment of gauge redundancy.

6.2 T2: one functor for logic, code, and physics

Theorem 29 (Curry–Howard–Lambek semantics of the pipeline). Let $T$ be a Martin-Löf dependent type theory with $Σ$ -, $Π$ -, and identity types, and let $Syn (T)$ be its syntactic category (objects: contexts; morphisms: substitutions up to definitional equality). For any locally cartesian closed category $C$ modelling $T$ there is an interpretation functor $[[-]] : Syn (T) ⟶ C$ sending types to objects and terms to (global) sections, and it is sound: it preserves the type-forming operations up to canonical isomorphism. Composing with a realization functor $R : C \to Phys$ yields a single composite $Syn (T) [[-]] C R Phys$ that interprets, simultaneously and by one categorical translation, the logical reading (propositions as types, proofs as terms), the computational reading (programs as terms, evaluation as normalization), and the physical reading (state spaces as types, processes as terms, realization as $R$ ).

Proof. The existence and soundness of $[[-]]$ is the Curry–Howard–Lambek/Seely correspondence between Martin-Löf type theory with $Σ, Π$ , and identity types and locally cartesian closed categories [5, 1, 2]: $Σ$ -types interpret as dependent sums (left adjoint to pullback), $Π$ -types as dependent products (right adjoint to pullback), and identity types as the relevant path objects; functoriality of $[[-]]$ is precisely the statement that substitution is interpreted by pullback and composes, i.e. soundness of the substitution calculus. Since functors compose (4), $R \circ [[-]]$ is a functor. The three readings are three names for the values of this one functor: the logical reading names the objects of $Syn (T)$ as propositions, the computational reading names its morphisms as programs, and the physical reading names $R$ applied to them as realizations. The equalities among these readings are literal equalities of the functor’s values, which is the content of the “theorem $=$ specification, proof $=$ implementation, physical process $=$ realization” slogan. ◻

Corollary 30 (Composition is quadruply the same law). Under 29, given $p : A \to B$ and $q : B \to C$ , the composite $q \circ p$ is simultaneously: logical-implication composition, proof/term composition, program composition, and—after $R$ —composition of physical processes. The associativity (3) of $\circ$ is one law shared by all four readings.

Proof. Immediate from 29: composition in $Syn (T)$ is substitution composition, sent by the two functors to composition in $C$ and then in $Phys$ ; each named reading is the same morphism under a different name, and associativity is inherited from 5. ◻

6.3 T3: no cloning forces encoding

Theorem 31 (Structural no-cloning). Let $C$ be a symmetric monoidal category and suppose there is a uniform copying operation: writing $D : C \to C \times C$ for the diagonal functor, a natural transformation $Δ : Id_{C} \Rightarrow \otimes \circ D$ with components $Δ_{A} : A \to A \otimes A$ , together with a natural deleting $⋄_{A} : A \to I$ , making each $A$ a cocommutative comonoid compatibly with $\otimes$ and the symmetry. Then $\otimes$ is a categorical product: $C$ is cartesian monoidal. Consequently, in $FdHilb$ —where the tensor product is not a categorical product—no such uniform copying exists, and quantum high availability cannot be replication.

Proof. The hypotheses are exactly Fox’s theorem: a symmetric monoidal category equipped with a natural, coherent, cocommutative comonoid structure $(Δ_{A}, ⋄_{A})$ on every object, compatible with $\otimes$ , is cartesian, with $\otimes$ the product, $I$ the terminal object, $⋄_{A}$ the unique map $A \to I$ , and $Δ_{A}$ the diagonal; naturality of $Δ$ and $⋄$ supplies the universal property of the product on morphisms. Now suppose, for contradiction, that $FdHilb$ admitted such a uniform copying. Then its monoidal product $\otimes$ would be the categorical product. But the categorical product (equivalently, in $FdHilb$ , the biproduct) of Hilbert spaces is the direct sum $\oplus$ , with $dim (A \oplus B) = dim A + dim B$ , whereas $dim (A \otimes B) = dim A \cdot dim B$ . For $dim A = dim B = 2$ these are $4$ and $4$ only coincidentally; taking $dim A = dim B = 3$ gives $6 \neq = 9$ , so $\otimes \neq ≅ \times$ as bifunctors. This contradiction shows no uniform natural copying exists in $FdHilb$ : the no-cloning theorem. Because copying is unavailable, protecting a quantum state cannot proceed by replication; the only representational option is an embedding $ι : H_{logical} ↪ H_{phys}$ into a larger physical Hilbert space—encoding—which is precisely Part VI’s quantum high-availability construction $H_{phys} ≃ H_{logical} \otimes H_{gauge} \oplus H_{error}$ . ◻

Remark 32 (Classical structures as the copiable objects). The objects of a dagger-compact category that do admit natural copying are exactly the classical structures: special commutative dagger-Frobenius algebras, whose comultiplication is a copying map. In $FdHilb$ these correspond to a choice of orthonormal basis—the “classical” pointer states one may copy. Thus T3 also explains why classical high availability (replication) works for classical data and fails for genuinely quantum data: only basis states are copiable [4].

6.4 T4: groupoid quotients are finer than set quotients

Theorem 33 (Truncation reconstruction of “stacks retain gauge information”). Let $G$ be a $0$ -type (a set carrying a group structure) acting on a $0$ -type (set) $X$ . Form the groupoid quotient (a higher inductive type) $X / / G$ , whose points are those of $X$ , with a path $x = g \cdot x$ for each $g : G$ , subject to the groupoid coherences. Then:

$X / / G$ is a $1$ -type, and for each $x$ the loop space $Ω_{x} (X / / G) ≃ Stab_{G} (x)$ retains the stabilizer as nontrivial automorphisms;
the set quotient $X / G$ is the $0$ -truncation $∥ X / / G ∥_{0}$ , which forgets exactly those stabilizer loops;
hence whenever some stabilizer is nontrivial, $X / / G$ is strictly finer than $X / G$ : there is no equivalence $X / / G ≃ X / G$ .

This is a purely type-theoretic reconstruction of the source proposition “stacks retain gauge information” ( $Aut_{[X / G]} (x) ≃ Stab_{G} (x)$ ) and of Part III’s finer-moduli phenomenon.

Proof. (a) By construction the only generating paths of $X / / G$ at a point $x$ are the $g \cdot (-)$ loops, and the higher inductive coherences make loop concatenation match group multiplication; the loops fixing $x$ are precisely those $g$ with $g \cdot x = x$ , i.e. $Stab_{G} (x)$ , giving $Ω_{x} (X / / G) ≃ Stab_{G} (x)$ . Since $G$ is a $0$ -type, each stabilizer $Stab_{G} (x) \subseteq G$ is a set, so every loop space is a set and $X / / G$ is $1$ -truncated; here the set hypotheses on $X$ and $G$ are exactly what bounds $X / / G$ at truncation level $1$ (a $G$ with higher homotopy, such as a delooped Lie group, would raise the level regardless of stabilizers). (b) The set quotient is defined as the $0$ -truncation of $X / / G$ (equivalently the quotient of $X$ by the orbit equivalence relation), and $0$ -truncation identifies all parallel paths, so all stabilizer loops collapse to reflexivity, retaining only orbits. (c) If some $Stab_{G} (x) \neq = {e}$ then $Ω_{x} (X / / G)$ is a nontrivial set while the corresponding loop space in the $0$ -type $X / G$ is contractible; an equivalence $X / / G ≃ X / G$ would induce an equivalence on loop spaces (equivalences preserve all homotopy structure), a contradiction. Reading a stabilizer loop as a residual gauge automorphism of the configuration $x$ , (a)–(c) are exactly the statement $Aut_{[X / G]} (x) ≃ Stab_{G} (x)$ with the coarse quotient forgetting $Aut$ , which is the source’s “stacks retain gauge information.” ◻

Corollary 34 (One fact, four proofs). The proposition “passing to the stack/groupoid quotient retains stabilizer data that the coarse quotient forgets” now has a type-theoretic proof (33) via truncation levels, complementing Part I’s informal gluing argument, Part III’s algebro-geometric moduli argument, and Part VI’s forthcoming descent-theoretic proof. These are one theorem with four proofs at increasing rigor—the headline “closure” motif of the synthesis paper.

The truncation tower relating the two quotients is:

X

X / / G

X / G

$X$ → $X / / G$ $quotient$
$X$ ↘ $X / G$ $orbit map$
$X / / G$ ↓ $X / G$ $∥ - ∥_{0}$

7 The category-theory and HoTT representation dictionary

We collect the core dictionary entries with S/H/P labels; the full longtables are in 12. The discipline is that of the whole series: an entry is $S$ when it is a standard mathematical fact used verbatim in mathematical physics, and $S/H$ or $H$ when its physical reading is a heuristic layer.

Category theory	Physical representation	Status
Object	Physical system / state space	S/H
Morphism $f : A \to B$	Process, transition, evolution	S
Composition $g \circ f$	Sequential process	S
Identity morphism	Do-nothing process	S
Isomorphism	Reversible equivalence	S
Equivalence of categories	Same theory, dual descriptions	S
Functor	Physical theory / quantization	S
Natural transformation	Uniform field redefinition	S/H
Monoidal product $\otimes$	Parallel composition of systems	S
Dagger-compact category	Quantum process calculus	S
Trace	Feedback / partition function	S/H
Yoneda lemma	System known by its probes	S/H

HoTT / type theory	Physical representation	Status
Type $A$	Space of states / possibilities	S/H
Term $a : A$	State / event / witness	S/H
Dependent type $B (x)$	Field / fibre over base point	S/H
Identity type $a = b$	Path / equivalence of states	S/H
Transport	Parallel transport / coordinate change	S/H
Equivalence $A ≃ B$	Duality / gauge-equivalent description	H
Univalence	Equivalent systems identified	S/H
$0$ -truncation	Classical coarse-graining	H
Groupoid quotient $X / / G$	Gauge configuration space	S/H
Circle HIT $S^{1}$	Winding / phase sector	H
Cohesive HoTT	Synthetic geometry for fields	S/H

8 Haskell formalization

The package src/category-theory-hott-composition/ encodes the composition/identity structures of 3, 4 and the groupoid-vs-set quotient of 33. We reproduce the type-class skeleton; the runnable Main.hs exercises the identity/associativity laws, a functor, a natural-transformation naturality check, a dagger-compact no-cloning obstruction, and the two quotients.

class Category cat where
identity :: cat a a
compose :: cat b c -> cat a b -> cat a c
class (Category c, Category d) => CFunctor c d f where
fmapC :: c a b -> d (f a) (f b)
newtype NatTrans d f g = NatTrans component :: forall a. d (f a) (g a)

Here NatTrans is parameterized by the target category d, so a natural transformation’s components are morphisms in d—not hardcoded Haskell functions—which keeps the encoding honest for non-Hask targets such as $FdHilb$ or $Bord_{n}$ .

Main.hs checks numerically that compose identity f == f == compose f identity for a concrete category (functions), that a chosen functor preserves composition, that a naturality square commutes, that the tensor-vs-biproduct dimension mismatch of 31 holds ( $2 \cdot 2 = 4$ but $3 \cdot 3 = 9 \neq = 6$ ), and that the groupoid quotient retains a stabilizer that the set quotient discards. The whole package compiles with ghc.

9 Lean formalization (best-effort sketch)

The directory lean/category-theory-hott-composition/ contains an idiomatic Lean 4 sketch capturing the category, functor, and identity-law types, plus signatures for T1 and T4. It reuses Mathlib’s CategoryTheory where convenient and states the physics-facing wrappers (a PhysicalCategory interpretation, a univalence-respects-realization signature, and a groupoid-quotient-finer-than-set-quotient signature). It is a best-effort sketch, not build-gated.

10 Discussion

10.0.0.1 Composition in the ladder.

Parts I–IV produced translations—abstraction, realization, observation, TQFT, homology—each of which is a functor. 4 shows the library was always a diagram in $Cat$ ; Part V simply names the ambient grammar. The associativity and unit laws (3)–(4) are the reason the pipeline may be assembled from stages at all, and 30 shows the same law governs logical, computational, and physical composition.

10.0.0.2 Identity in the ladder.

Part I postulated that equivalent representations carry the same physical content (Axiom Equivalence). 27 derives it for every internally definable realization, and 28 reads the residue—realizations that fail it—as exactly the gauge-dependent quantities. This is the module’s central payoff: identity of structures, formalized by univalence, is the correct home for the “same physics, different description” principle that recurs through the series.

10.0.0.3 Forecasting Part VI.

31 forces quantum high availability to be encoding, and 33 produces the stabilizer-retention phenomenon inside the truncation hierarchy. Both are the categorical/type-theoretic inputs Part VI turns into stacks (groupoid-valued sheaves) and quantum error-correcting codes. 34 records that the stabilizer-retention fact will then have four proofs at increasing rigor—the synthesis paper’s “closure theorem.”

10.0.0.4 Limitations.

Category theory and HoTT are status S mathematics; their physical readings carry the flags of 7. We reiterate the series limitations in this module’s terms. (i) We claim no single universal functor $Math \to Phys$ ; 4 is domain-indexed by $d$ , matching Part I’s deliberate locality. (ii) The reading of a type as a “space of physical possibilities” is heuristic (status $H$ ). (iii) 27 requires a genuinely univalent model and an internally definable realization; externally chosen realizations are outside its scope by design, which is the gauge-dependence caveat, not a defect. (iv) The no-cloning argument is stated for $FdHilb$ ; infinite-dimensional refinements need additional analytic hypotheses. (v) Univalence is a foundational axiom (with computational content in cubical type theory) rather than a physical measurement, so its physical reading remains $S/H$ .

11 Conclusion

Part V isolates the compositional glue of the representation library. Category theory supplies the laws of composition: associativity, units, functoriality, naturality, the interchange law, and (via Eckmann–Hilton) the first constraint linking two compositions through a shared identity. HoTT supplies the theory of identity: identity types as paths, path induction as the sole generator of transport, and univalence as the identification of identity with equivalence. Four theorems give the physics. Univalence turns Part I’s Equivalence axiom into a theorem (T1); the Curry–Howard–Lambek correspondence exhibits one functor interpreting logic, code, and physics (T2); a structural no-cloning theorem forces quantum high availability to be encoding (T3); and the groupoid quotient’s strict refinement of the set quotient reconstructs “stacks retain gauge information” inside the truncation hierarchy (T4). Together they make explicit the universal grammar that Parts I–IV used implicitly and that Part VI will use to build stacks and quantum codes. In the compressed slogans of the series, mathematics is the syntax of physical representation and categories/types are the grammar of its composition and identity.

[1] S. Mac Lane, Categories for the Working Mathematician, Graduate Texts in Mathematics 5, 2nd ed., Springer, 1998.

[2] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013.

[3] J. C. Baez and M. Stay, Physics, topology, logic and computation: A Rosetta Stone, arXiv:0903.0340 (2009); Lecture Notes in Physics 813 (2010), 95–172.

[4] S. Abramsky and B. Coecke, A categorical semantics of quantum protocols, arXiv:quant-ph/0402130 (2004); Proc. 19th IEEE Symposium on Logic in Computer Science (LiCS), 2004.

[5] J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics 7, Cambridge University Press, 1986.

[6] J. Lurie, On the classification of topological field theories, arXiv:0905.0465 (2009); Current Developments in Mathematics 2008, 129–280.

[7] J. Lurie, Higher Topos Theory, Annals of Mathematics Studies 170, Princeton University Press, 2009.

[8] U. Schreiber, Differential cohomology in a cohesive $\infty$ -topos, arXiv:1310.7930 (2013).

[9] E. Riehl and D. Verity, Elements of $\infty$ -Category Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2022.

[10] M. Atiyah, Topological quantum field theories, Publications Mathématiques de l’IHÉS 68 (1988), 175–186.

[11] E. Riehl, Category Theory in Context, Aurora: Dover Modern Math Originals, Dover Publications, 2017.

12 Full category-theory and HoTT representation library

The following longtables reproduce the module’s dictionary (source Appendix E), with epistemic status labels carried verbatim. Each row is a representation entry $(M, P, τ, σ)$ in the sense of 1.

Category theory library (physical representation dictionary).
Category theory	Physical representation	Semantic meaning	Status
Object	Physical system / state space	Thing capable of processes	S/H
Morphism $f : A \to B$	Process, transition, evolution	Physical transformation	S
Composition $g \circ f$	Sequential process	One process after another	S
Identity morphism	Do-nothing process	Persistence / trivial evolution	S
Isomorphism	Reversible equivalence	Same structure, new coordinates	S
Equivalence of categories	Same theory structurally	Dual physical descriptions	S
Functor	Translation between worlds	Physical theory / quantization	S
Natural transformation	Uniform deformation	Theory equivalence / field redefinition	S/H
Category of states	State-system universe	Objects systems, arrows evolutions	H
Category of observables	Measurement-algebra universe	Arrows observable transformations	H
Monoidal category	Parallel composition	Composite systems	S
Tensor product $\otimes$	Combine systems	Parallel physical composition	S
Unit object $I$	Vacuum / trivial system	No-system baseline	S/H
Symmetric monoidal	Exchangeable systems	Bosonic-like swap symmetry	S/H
Braided monoidal	Nontrivial exchange	Anyonic / braided statistics	S
Ribbon category	Braiding plus twist	Topological quantum computation	S
Compact closed	Dualizable inputs/outputs	Process–state duality	S
Dagger category	Reversal / adjoint	Quantum adjoint, time reversal	S
Dagger-compact	Quantum process calculus	Teleportation, cups/caps	S
String diagram	Diagrammatic process	Circuit / Feynman grammar	S
Trace	Feedback loop	Closed process, partition function	S/H
Dual object $A^{*}$	Antisystem / dual space	Bra/ket, particle/antiparticle	S/H
Evaluation map	Pairing	Measurement, annihilation	S/H
Coevaluation map	Pair creation	Entangled pair / vacuum insertion	S/H
Limit	Universal compatible solution	Constraint satisfaction	S
Colimit	Universal gluing	Global system from parts	S
Pullback	Fibered constraint	Simultaneous conditions	S
Pushout	Gluing along boundary	Coupled systems	S
Adjunction $F ⊣ G$	Dual translation pair	Free/forgetful, prep/measure	S/H
Monad	Dynamics with effects	State update, computation effect	S/H
Comonad	Context extraction	Observation / coarse environment	H
Algebra over monad	System obeying effects	Dynamics closed under update	H
Coalgebra	State-transition system	Observable unfolding / branching	S/H
Operad	Multi-input composition law	Interaction vertices / couplings	S
PROP	Multi-in/out network	Circuit / Feynman process algebra	S
Enriched category	Structured hom-spaces	Distances, probabilities, Hilbert homs	S/H
2-category	Objects, processes, transformations	Theories, defects, transformations	S
$\infty$ -category	All higher coherences	Histories, higher gauge data	S
Higher category	Nested process hierarchy	Particles, strings, branes, defects	S
$n$ -category	$n$ -level process system	Extended TQFT codimension	S
Topos	Universe of variable sets	Contextual world of observation	H
Sheaf topos	Local-to-global universe	Observer-dependent gluing	S/H
Internal language	Logic of a category	Native reasoning of a universe	H
Yoneda lemma	Object known by probes	System determined by observations	S/H

Homotopy type theory library (physical representation dictionary).
HoTT / type theory	Physical representation	Semantic meaning	Status
Type $A$	Space of states / propositions	Domain of possible inhabitants	S/H
Term $a : A$	State / event / witness	Actual instance of a possibility	S/H
Dependent type $B (x)$	Fibre over configuration	Field degrees over base point	S/H
$Σ$ -type	Total space	Configuration plus dependent data	S
$Π$ -type	Space of sections	Field assigning data everywhere	S
Identity type $a = b$	Path from $a$ to $b$	Equivalence / evolution of states	S/H
Higher identity type	Homotopy between paths	Coherence between evolutions	S/H
Path induction	Reasoning from identity	Transport laws from equivalence	S/H
Transport	Move structure along path	Parallel transport / coordinate change	S/H
Equivalence $A ≃ B$	Same physics, new representation	Duality / gauge equivalence	H
Univalence	Equivalence treated as identity	Equivalent systems identified	S/H
Universe $U$	Type of systems / theories	Meta-space of descriptions	H
Higher inductive type	Generated points/paths/cells	Synthetic topological spaces	S/H
Circle HIT $S^{1}$	Generated loop space	Winding sector / phase circle	H
Sphere HIT $S^{n}$	Generated $n$ -charge carrier	Higher topological charge	H
Pushout type	Glued system	Boundary coupling / fusion	S/H
Pullback type	Constraint-matched system	Simultaneous compatibility	S/H
Quotient type	Identified states	Gauge quotient / equivalence classes	H
Truncation	Forget higher identity	Classical approximation	H
Mere proposition	Yes/no observable	Proof-irrelevant physical fact	H
Set-truncation	Classical state set	No higher path information	H
Groupoid level	Gauge-state structure	States plus equivalences	S/H
$\infty$ -groupoid	Full homotopy state space	States, paths, paths-between-paths	S/H
Contractible type	Unique state up to equivalence	Trivial phase / vacuum sector	H
Fiber sequence	Structured dependency	Gauge fibre over base	S/H
Modal type theory	Observation / filtering modes	Coarse-graining, localization	H
Cohesive HoTT	Synthetic smooth geometry	Internal language for fields	S/H
Shape modality	Underlying homotopy type	Forget geometry, keep topology	S/H
Flat modality	Discrete / codified form	Locally constant representation	H
Sharp modality	Codiscrete / crisp form	Purely formal / global representation	H
Differential cohesion	Smooth infinitesimal structure	Synthetic differential geometry	S/H

Download PDF