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

## Summary

Phase 2b of the standards#203 trusted-base rollout. Cluster: CNO common
— `proofs/coq/category/CNOCategory.v` (1 marker).

The single axiom `hom_functor` was classified **DISCHARGE** in #58
Phase 1 triage. The file's existing leading comment (L312–322) records
the rationale for current axiomatisation:

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.

## Disposition
- §(d) DEBT, INDEFINITE deadline (blocked on `SetCategory` scaffolding).
- No inline annotation needed for §(d) per the policy schema —
  documentation is via file-path mention in `docs/proof-debt.md`.

## Note on cluster size

The picked "CNO common" cluster was originally Coq `common/CNO.v` (4
axioms) + `category/CNOCategory.v` (1). The 4 axioms in `common/CNO.v`
were discharged in #24 / #32 prior to this rollout, so the cluster is
effectively a one-axiom mop-up.

## Verification

```
$ bash ../standards/scripts/check-trusted-base.sh .
[INFO] Found 129 soundness-relevant escape hatch(es).
[ERROR] 122/129 escape hatch(es) are undocumented.
```

Down from 123 after PR #60 (Lambda). Cumulative: 7 markers now
documented (Lambda 5 + CNOCategory 1 + 1 other already-passing).

Refs standards#203, #58, #60.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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`