---

Step * of Lemma mk-groupoid_wf

∀[C:SmallCategory]. ∀[inv:x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) x y) ⟶ (cat-arrow(C) y x)].
  Groupoid(C;
           inv(x,y,f) = inv[x;y;f]) ∈ Groupoid 
  supposing ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
              (((cat-comp(C) x y x f inv[x;y;f]) = (cat-id(C) x) ∈ (cat-arrow(C) x x))
              ∧ ((cat-comp(C) y x y inv[x;y;f] f) = (cat-id(C) y) ∈ (cat-arrow(C) y y)))
BY
{ (ProveWfLemma THEN MemTypeCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[inv:x:cat-ob(C)  {}\mrightarrow{}  y:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  x  y)  {}\mrightarrow{}  (cat-arrow(C)  y  x)].
    Groupoid(C;
                      inv(x,y,f)  =  inv[x;y;f])  \mmember{}  Groupoid 
    supposing  \mforall{}x,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.
                            (((cat-comp(C)  x  y  x  f  inv[x;y;f])  =  (cat-id(C)  x))
                            \mwedge{}  ((cat-comp(C)  y  x  y  inv[x;y;f]  f)  =  (cat-id(C)  y)))


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index