This page provides an index of machine-checked formalizations of mathematical constructions documented on the nLab.
The index is organized by mathematical subject rather than by proof assistant. Formal verification and human semantic review are recorded separately.
Homogeneous path type (FI-001)
nLab: identity type Classification: plausible structural correspondence. Dependent path type (FI-002)
nLab: identity type Classification: partial correspondence; the nLab discussion is broader than the primitive presentation. Path composition (FI-003)
nLab: equality in type theory (Typal equality, Transitivity) Classification: plausible structural correspondence. Identity-system characterization (FI-004)
nLab: equality in type theory Classification: partial correspondence; not the same construction as path inversion. Dependent total space (FI-005)
nLab: dependent type
Correspondence evidence: Both constructions represent dependent sums. This does not imply a classical lifting-property fibration. Homotopy fiber of a map (FI-006)
nLab: homotopy fiber
Correspondence evidence: The Agda declaration defines the fiber using dependent pairs and paths to the specified point. Fiber of a dependent total-space projection (FI-007)
nLab: homotopy pullback
Correspondence evidence: The formal declaration establishes the homotopy-fiber equivalence for the projection of a dependent total space; this is a specific instance related to the homotopy-pullback construction, not a formalization of every homotopy pullback. The construction of monodromy in homotopy type theory can be expressed through transport along paths in dependent type families. Formalization: Transport equivalences, loop-space monodromy, pointed transport, and induced equivalences on higher homotopy groups. Verification: Agda 2.8.0, Cubical Library v0.9 — type-checked. Human mathematical and semantic review: Pending. Scope limitation: The complete fundamental-group action on fixed-basepoint higher homotopy groups has not yet been formalized.Homotopy theory
Paths and identity types
Cubical Agda: Cubical.Core.Primitives.Path
Scope: Homogeneous path type Path A a b.
Source: Pinned Agda source
Machine verification: source verified; not independently rebuilt.
Human semantic review: pending.
Cubical Agda: Cubical.Core.Primitives.PathP
Scope: Dependent paths in a family over the cubical interval.
Source: Pinned Agda source
Machine verification: source verified; primitive not independently rebuilt.
Human semantic review: pending.
Cubical Agda: Cubical.Foundations.Prelude._∙_
Scope: Composition of paths, first p, then q.
Source: Pinned Agda source
Machine verification: source verified; not independently rebuilt.
Human semantic review: pending.
1Lab: 1Lab.Path.IdentitySystem.identity-system-gives-path
Scope: An identity-system witness yields an equivalence R a b ≃ (a ≡ b).
Source: Official documentation (revision d45acb1d16acb2472ade6f1cfbad4ba00867ad1c)
Machine verification: source verified; no 1Lab build reproduced.
Human semantic review: pending.Dependent total spaces, homotopy fibers, and pullbacks
Cubical Agda: Cubical.Core.Primitives.Σ (re-exported by Cubical.Data.Sigma)
Scope: Dependent sums of type families.
Source: Pinned Agda source
Machine verification: source verified; primitive not independently rebuilt.
Human semantic review: pending.
Cubical Agda: Cubical.Foundations.Equiv.Base.fiber
Scope: Homotopy fiber of a map f : A → B over a point y : B.
Source: Pinned Agda source
Machine verification: source verified; not independently rebuilt.
Human semantic review: pending.
Cubical Agda: NLabMonodromy.total-hofib≃
Scope: The equivalence fiber (total-projection P) b ≃ P b.
Source: Verified Agda implementation
Machine verification: independently type-checked by the pilot.
Human semantic review: pending.
Monodromy — Cubical Agda
Last revised on November 9, 2026 at 19:43:13. See the history of this page for a list of all contributions to it.