From 53f292abe8d0eb535f9bd496599794639903aeac Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 09:23:54 +0100 Subject: [PATCH] =?UTF-8?q?docs:=20enumerate=20CNOCategory.v=20hom=5Ffunct?= =?UTF-8?q?or=20as=20=C2=A7(d)=20DEBT=20(Phase=202b)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase 2b of the standards#203 trusted-base rollout. Cluster: CNO common — `proofs/coq/category/CNOCategory.v` (1 marker). The single axiom `hom_functor : forall (C : Category) (A : @Obj C), Functor C C` was classified DISCHARGE in #58 Phase 1 triage. The file's leading comment (L312-322) already records why it's axiomatised today: 1. `yoneda_cno` is already proven without it. 2. The proper signature `Functor C SetCategory` needs a SetCategory instance, which requires universe-polymorphism machinery. 3. The conceptual result (CNOs = identity under Yoneda) stands. This PR adds the corresponding §(d) DEBT entry with owner + INDEFINITE deadline (blocked on SetCategory scaffolding). The Coq common namespace `proofs/coq/common/CNO.v` has zero axioms (the 4 historical ones were discharged in #24 / #32). Verification: `check-trusted-base.sh` now reports 122 undocumented (down from 123). The CNOCategory.v entry is documented via file-path mention in `docs/proof-debt.md` (no inline annotation needed for §(d) DEBT items per the policy schema). Refs standards#203, #58. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/proof-debt.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/docs/proof-debt.md b/docs/proof-debt.md index c032314..848921c 100644 --- a/docs/proof-debt.md +++ b/docs/proof-debt.md @@ -70,6 +70,21 @@ After Phase 1, the §(d) bucket contains only the Lean axioms and 7 Idris2 postulates that have not yet been triaged. Coq markers are no longer in §(d). +### Coq — provable, awaiting proof + +- `proofs/coq/category/CNOCategory.v:323` — `hom_functor` + - **Owner**: @hyperpolymath + - **Plan**: replace `Axiom hom_functor : ... Functor C C` with the + proper Yoneda construction `Functor C SetCategory`. The + file's leading comment (L312-322) records why this is currently + axiomatised: (1) `yoneda_cno` is already proven without it, + (2) `SetCategory` needs universe-polymorphism machinery, + (3) the conceptual claim stands. + - **Triage**: classified DISCHARGE in `docs/proof-debt-triage.md` + (Phase 1, #58). + - **Deadline**: INDEFINITE (blocked on `SetCategory` instance — + universe-polymorphism scaffolding precondition). + ### Lean — provable, awaiting proof - `proofs/lean4/LambdaCNO.lean:183` — `subst_closed_term`