Towards Coherence Depth Two for Cubical Sealed Extensions

This archive contains the LMCS artifact package for “Coherence Depth Two for Cubical Sealed Extensions”. The artifact accompanies the LMCS submission version of the paper and provides the theorem-facing materials needed to inspect and check the formal and computational claims referenced by the article. It includes the LMCS paper source and PDF, Cubical Agda modules, theorem-map metadata, audit scripts, trust-boundary documentation, and small case-study fixtures. The Agda development is intentionally theorem-facing rather than a full mechanization of every expository statement in the paper. The included theorem map records which paper claims are directly represented by Agda declarations, which are supported by audit scripts or fixtures, and which remain paper-level or conditional on stated modeling assumptions. The archive is designed to be checked with the included artifact script. The corresponding GitHub archival tag is `v0.1.2-lmcs-artifact`, and the hosted GitHub Actions artifact-check run for that tag passed at: https://github.com/efficient-novelty/coherence-depth/actions/runs/25963679151 Reserved Zenodo DOI: https://doi.org/10.5281/zenodo.20235005