docs: enumerate CNOCategory.v hom_functor as §(d) DEBT (Phase 2b)

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) <noreply@anthropic.com>

Author: hyperpolymath

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`