---

Step * 1 of Lemma groupoids_wf


Cat(ob = Groupoid;
    arrow(G,H) = groupoid-map(G;H);
    id(G) = 1;
    comp(G,H,K,F,G) = functor-comp(F;G)) ∈ SmallCategory'
BY
{ (BLemma `mk-cat_wf` THEN Try (QuickAuto)) }

1
.....wf..... 
λG.1 ∈ x:Groupoid ⟶ groupoid-map(x;x)

2
.....wf..... 
λG,H,K,F,G. functor-comp(F;G) ∈ x:Groupoid
⟶ y:Groupoid
⟶ z:Groupoid
⟶ groupoid-map(x;y)
⟶ groupoid-map(y;z)
⟶ groupoid-map(x;z)

3
∀G,H:Groupoid. ∀F:groupoid-map(G;H).
  ((functor-comp(1;F) = F ∈ groupoid-map(G;H)) ∧ (functor-comp(F;1) = F ∈ groupoid-map(G;H)))

4
∀G,H,z,K:Groupoid. ∀F:groupoid-map(G;H). ∀G1:groupoid-map(H;z). ∀h:groupoid-map(z;K).
  (functor-comp(functor-comp(F;G1);h) = functor-comp(F;functor-comp(G1;h)) ∈ groupoid-map(G;K))

---

Latex:

---

Latex:

Cat(ob  =  Groupoid;
        arrow(G,H)  =  groupoid-map(G;H);
        id(G)  =  1;
        comp(G,H,K,F,G)  =  functor-comp(F;G))  \mmember{}  SmallCategory'


By

---

Latex:
(BLemma  `mk-cat\_wf`  THEN  Try  (QuickAuto))

---

Home Index