Step * of Lemma cat-comp-ident

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


Latex:


Latex:
\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:
((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