II.T36 — Tau-Yoneda Embedding

The Yoneda functor y: tau -> [tau^op, tau] is fully faithful: (1) well-defined with internal target via self-enrichment, (2) faithful by evaluation at id, (3) full via Code/Decode computable witnesses, (4) bipolar-preserving under the e_+/e_- decomposition.