Step
*
of Lemma
name-cat_wf
NameCat ∈ SmallCategory
BY
{ (Unfolds ``name-cat small-category`` 0 THEN At ⌜𝕌'⌝ MemTypeCD⋅ THEN Auto THEN All Reduce THEN Auto) }
Latex:
Latex:
NameCat  \mmember{}  SmallCategory
By
Latex:
(Unfolds  ``name-cat  small-category``  0  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Auto  THEN  All  Reduce  THEN  Auto)
Home
Index