---

Step * of Lemma groupoid-nerve-functor-flip

∀[G:Groupoid]. ∀[I:Cname List]. ∀[u:nameset(I)]. ∀[K:Cname List]. ∀[f:name-morph(I;K)]. ∀[f1:name-morph(K;[])].
  ∀x1:nameset(I)
    ∀[F:Functor(poset-cat(I-[x1]);cat(G))]
      (F (f o f1) flip((f o f1);u) (λx.Ax))
      = (f(F) f1 flip(f1;f u) (λx.Ax))
      ∈ (cat-arrow(cat(G)) (F (f o f1)) (F (f o flip(f1;f u)))) 
      supposing (↑isname(f u)) ∧ ((f1 (f u)) = 0 ∈ ℕ2)
BY
{ (RepeatFor 8 (Intro) THEN D 0) }

1
1. G : Groupoid
2. I : Cname List
3. u : nameset(I)
4. K : Cname List
5. f : name-morph(I;K)
6. f1 : name-morph(K;[])
7. x1 : nameset(I)
8. F : Functor(poset-cat(I-[x1]);cat(G))
9. (↑isname(f u)) ∧ ((f1 (f u)) = 0 ∈ ℕ2)
⊢ (F (f o f1) flip((f o f1);u) (λx.Ax))
= (f(F) f1 flip(f1;f u) (λx.Ax))
∈ (cat-arrow(cat(G)) (F (f o f1)) (F (f o flip(f1;f u))))

2
.....wf..... 
1. G : Groupoid
2. I : Cname List
3. u : nameset(I)
4. K : Cname List
5. f : name-morph(I;K)
6. f1 : name-morph(K;[])
7. x1 : nameset(I)
8. F : Functor(poset-cat(I-[x1]);cat(G))
⊢ istype((↑isname(f u)) ∧ ((f1 (f u)) = 0 ∈ ℕ2))

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  \mforall{}[I:Cname  List].  \mforall{}[u:nameset(I)].  \mforall{}[K:Cname  List].  \mforall{}[f:name-morph(I;K)].
\mforall{}[f1:name-morph(K;[])].
    \mforall{}x1:nameset(I)
        \mforall{}[F:Functor(poset-cat(I-[x1]);cat(G))]
            (F  (f  o  f1)  flip((f  o  f1);u)  (\mlambda{}x.Ax))  =  (f(F)  f1  flip(f1;f  u)  (\mlambda{}x.Ax)) 
            supposing  (\muparrow{}isname(f  u))  \mwedge{}  ((f1  (f  u))  =  0)


By

---

Latex:
(RepeatFor  8  (Intro)  THEN  D  0)

---

Home Index