---

Step * of Lemma trans-id-property

No Annotations
∀C1,C2:SmallCategory. ∀x,y:Functor(C1;C2). ∀f:nat-trans(C1;C2;x;y).
  ((identity-trans(C1;C2;x) o f = f ∈ nat-trans(C1;C2;x;y)) ∧ (f o identity-trans(C1;C2;y) = f ∈ nat-trans(C1;C2;x;y)))
BY
{ TACTIC:(Auto
          THEN DVar `f'
          THEN Symmetry
          THEN EqTypeCD
          THEN Auto
          THEN Ext
          THEN Auto
          THEN RepUR ``trans-comp identity-trans`` 0
          THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C1,C2:SmallCategory.  \mforall{}x,y:Functor(C1;C2).  \mforall{}f:nat-trans(C1;C2;x;y).
    ((identity-trans(C1;C2;x)  o  f  =  f)  \mwedge{}  (f  o  identity-trans(C1;C2;y)  =  f))


By

---

Latex:
TACTIC:(Auto
                THEN  DVar  `f'
                THEN  Symmetry
                THEN  EqTypeCD
                THEN  Auto
                THEN  Ext
                THEN  Auto
                THEN  RepUR  ``trans-comp  identity-trans``  0
                THEN  Auto)

---

Home Index