---

Step * of Lemma cat-comp-ident

No Annotations
∀[C:SmallCategory]
  ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
    (((cat-comp(C) x x y (cat-id(C) x) f) = f ∈ (cat-arrow(C) x y))
    ∧ ((cat-comp(C) x y y f (cat-id(C) y)) = f ∈ (cat-arrow(C) x y)))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN D 1
          THEN RepeatFor 3 (D -5)
          THEN All
          (RepUR ``cat-comp cat-arrow cat-ob cat-id``)⋅
          THEN All Reduce
          THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory]
    \mforall{}x,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.
        (((cat-comp(C)  x  x  y  (cat-id(C)  x)  f)  =  f)  \mwedge{}  ((cat-comp(C)  x  y  y  f  (cat-id(C)  y))  =  f))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  D  1
                THEN  RepeatFor  3  (D  -5)
                THEN  All
                (RepUR  ``cat-comp  cat-arrow  cat-ob  cat-id``)\mcdot{}
                THEN  All  Reduce
                THEN  Auto)

---

Home Index