失敗録:Δで考えると向き辻褄が合わない→トレースだ！

みたいなのを定義してやればいいのでは？

を疎かにしているのが露呈している

sig EnrichedCategory in CAT @ %
  Data
    -1-sig
      MonoidalCategory V ⊗ i α λ ρ
    %0-morph
      .0-morph @ Ob : Class
    %1-morph
      hom : Ob^op × Ob -> V

    %2-morph
      "identity element" @ id
        : ! * i => Δ * hom
        : Ob -> V

      "composition morphism" @ comp
        : Ob^ × Δ × Ob^ ; hom ⊗ hom
          => Ob^ × ! × Ob^ ; hom
        : Ob × Ob × Ob -> V
  Axioms
    %3-eq "associative"
      comp ⊗ hom^; comp 
        =(hom×hom×hom)α; hom^ ⊗ comp; comp 
      : Ob^ × Δ × Δ × Ob^; (hom⊗hom)⊗hom 
        => Ob^ × ! × ! × Ob^ ; hom
      : Ob × Ob × Ob × Ob -> V
    %3-eq "left unital"
      : ⊗ hom