---

Step * of Lemma groupoid-right-cancellation

∀[G:Groupoid]. ∀[x,y,z:cat-ob(cat(G))]. ∀[a,b:cat-arrow(cat(G)) x y]. ∀[c:cat-arrow(cat(G)) y z].
  uiff((cat-comp(cat(G)) x y z a c) = (cat-comp(cat(G)) x y z b c) ∈ (cat-arrow(cat(G)) x z);a
  = b
  ∈ (cat-arrow(cat(G)) x y))
BY
{ 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)) x y
6. b : cat-arrow(cat(G)) x y
7. c : cat-arrow(cat(G)) y z
8. (cat-comp(cat(G)) x y z a c) = (cat-comp(cat(G)) x y z b c) ∈ (cat-arrow(cat(G)) x z)
⊢ a = b ∈ (cat-arrow(cat(G)) x y)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index