Constructive Covering Theory: Čech Cocycles, Local Systems, and Their Equivalence in Cubical Agda

Constructive Covering Theory: Čech Cocycles, Local Systems, and Their Equivalence in Cubical Agda We give a constructive formulation of covering theory in Homotopy TypeTheory (HoTT), with a complete machine verification in Cubical Agda. The central result is a pointwise equivalence of types TotalFiber (Cov, Loc→Cocycle (Cov, L), x) ≃ carrier (F (x) ) for any covering Cov, local system L, and base point x, established constructively and machine-verified across six Cubical Agdamodules (--safe --cubical --guardedness, zero postulates). --- CONTRIBUTIONS (i) Explicit Čech-cocycle-based construction. Rather than deriving monodromy from a pre-existing covering, Čech 1-cocycles serve as explicit generative data: the total fiber TotalFiber is constructed from cocycle data, and the covering structure emerges from local transition functions. (ii) Type-theoretic enforcement of Independence. The Independence Lemma — ensuring the construction is independentof local trivialization choices — is incorporated as a built-incoherence condition enforced by the type of rec→Set, not proved as a separate theorem. Well-definedness of the map `from` is a structural requirementthat must be satisfied for the function to be definable at all. (iii) Complete machine verification with zero postulates. The entire development compiles in Cubical Agda under--safe --cubical --guardedness with zero postulates across all six modules. The equivalence Cocycle Cov ≃ LocalSystem-at Cov isestablished constructively and machine-verified. --- OPEN PROBLEM (logically independent) An Ext¹–H¹ correspondence (Open Problem A) — the existence of a naturalmap ΦX: Ext¹ (X, X) → H¹ (U, Aut (V) ) compatible with classifying maps —is logically independent of the main result and left for future work. This problem requires additional algebraic structure not assumedin the present framework. --- CENTRAL PRINCIPLE Cocycles do not merely classify coverings; they generate them. The failure of local data to be globally consistent — measured bythe Independence Lemma — can be understood as a structural mechanismunderlying the construction of the total fiber. In this sense, the present paperprovides a type-theoretic formulation corresponding to the principle: Local compatibility constraints → Global geometric existence. --- FORMALIZATION Available at: https: //github. com/Psypher33/UMIN Modules (all --safe, zero postulates): UMINRHBase. agda — base types and coverings UMINRHFiber. agda — fiber construction UMINRHTotalFiberTriv. agda — trivialization lemmas UMINRHEquivFinal. agda — from / to / sec / ret / equiv UMINRHCocycleToLoc. agda — Loc→Cocycle / Independence UMINRHTheoremB. agda — Cocycle Cov ≃ LocalSystem-at Cov --- RELATED WORKS DOI 10. 5281/zenodo. 19385944 Homotopy-Theoretic Structures of Integrability, Thermal Time, and Coverings via Extension Classes (UMIN v1. 9. 1) DOI 10. 5281/zenodo. 19434808 Noncommutative Covering Theory via Fiber Functors: Extension Classes, Monodromy, and the UMIN Framework (v1. 7) DOI 10. 5281/zenodo. 19325080 Tor₁ and Cohomological Phantom Anomalies in PT-Symmetric Systems DOI 10. 5281/zenodo. 19125989 E₈ Cluster Geometry, Mixed Tate Motives, and p-adic Defects --- MSC 2020: 18N60, 55R05, 55P20, 03B38 Keywords: Homotopy Type Theory, Cubical Agda, covering theory, Čech cocycle, local system, higher inductive type, constructive mathematics, dependent type theory, Independence Lemma, zero postulates