---

Step * of Lemma edge-arrows-commute_wf

∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)
                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} 
                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).
  (edge-arrows-commute(C;I;L;E) ∈ ℙ)
BY
{ TACTIC:(Auto
          THEN Unfold `edge-arrows-commute` 0
          THEN Unfolds ``prop all implies`` 0
          THEN RepeatFor 4 ((PrimMemCD THENL [Auto; Id]))) }

1
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}  ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. x : name-morph(I;[])
6. i : {i:nameset(I)| (x i) = 0 ∈ ℕ2} 
7. j : {i:nameset(I)| (x i) = 0 ∈ ℕ2} 
8. ¬(i = j ∈ nameset(I))
⊢ (cat-comp(C) (L x) (L flip(x;i)) (L flip(flip(x;i);j)) (E i x) (E j flip(x;i)))
  = (cat-comp(C) (L x) (L flip(x;j)) (L flip(flip(x;j);i)) (E j x) (E i flip(x;j)))
  ∈ (cat-arrow(C) (L x) (L flip(flip(x;i);j))) ∈ Type

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}I:Cname  List.  \mforall{}L:name-morph(I;[])  {}\mrightarrow{}  cat-ob(C).  \mforall{}E:i:nameset(I)
                                                                                                                                            {}\mrightarrow{}  c:\{c:name-morph(I;[])| 
                                                                                                                                                        (c  i)  =  0\} 
                                                                                                                                            {}\mrightarrow{}  (cat-arrow(C)  (L  c) 
                                                                                                                                                    (L  flip(c;i))).
    (edge-arrows-commute(C;I;L;E)  \mmember{}  \mBbbP{})


By

---

Latex:
TACTIC:(Auto
                THEN  Unfold  `edge-arrows-commute`  0
                THEN  Unfolds  ``prop  all  implies``  0
                THEN  RepeatFor  4  ((PrimMemCD  THENL  [Auto;  Id])))

---

Home Index