---

Step * of Lemma groupoid-left-cancellation

No Annotations
∀[G:Groupoid]. ∀[x,y,z:cat-ob(cat(G))]. ∀[a,b:cat-arrow(cat(G)) y z]. ∀[c:cat-arrow(cat(G)) x y].
  uiff((cat-comp(cat(G)) x y z c a) = (cat-comp(cat(G)) x y z c b) ∈ (cat-arrow(cat(G)) x z);a
  = b
  ∈ (cat-arrow(cat(G)) y z))
BY
{ TACTIC:Auto }

1
1. G : Groupoid
2. x : cat-ob(cat(G))
3. y : cat-ob(cat(G))
4. z : cat-ob(cat(G))
5. a : cat-arrow(cat(G)) y z
6. b : cat-arrow(cat(G)) y z
7. c : cat-arrow(cat(G)) x y
8. (cat-comp(cat(G)) x y z c a) = (cat-comp(cat(G)) x y z c b) ∈ (cat-arrow(cat(G)) x z)
⊢ a = b ∈ (cat-arrow(cat(G)) y z)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:Groupoid].  \mforall{}[x,y,z:cat-ob(cat(G))].  \mforall{}[a,b:cat-arrow(cat(G))  y  z].  \mforall{}[c:cat-arrow(cat(G))  x  y].
    uiff((cat-comp(cat(G))  x  y  z  c  a)  =  (cat-comp(cat(G))  x  y  z  c  b);a  =  b)


By

---

Latex:
TACTIC:Auto

---

Home Index