---

Step * 2 2 1 1 1 1 1 1 1 1 2 1 1 of Lemma fillterm_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. j : {j:ℕ| ¬j ∈ I+i} 
6. rho : Gamma(I+i)
7. phi : 𝔽(I)
8. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
9. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
10. (i=0) ∈ 𝔽(I+i)
11. I ⊆ I+i+j
12. K : fset(ℕ)
13. J : fset(ℕ)
14. g : J ⟶ K
15. f : I+i+j,s(fl-join(I+i;s(phi);(i=0)))(K)
16. ¬((f i) = 0 ∈ Point(dM(K)))
17. f ∈ K ⟶ I+i+j
18. (((phi)<s>)<s>)<f> = 1 ∈ Point(face_lattice(K))
19. (s(phi) m(i;j) ⋅ f) = 1
20. (f ⋅ g i) = 0 ∈ Point(dM(J))
21. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
22. (i0) ⋅ s ⋅ s ⋅ f ⋅ g = m(i;j) ⋅ f ⋅ g ∈ J ⟶ I+i
⊢ (phi)<s ⋅ s ⋅ f ⋅ g> = 1 ∈ Point(face_lattice(J))
BY
{ RepeatFor 2 ((RWO "fl-morph-comp2<" 0 THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. j : {j:ℕ| ¬j ∈ I+i} 
6. rho : Gamma(I+i)
7. phi : 𝔽(I)
8. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
9. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
10. (i=0) ∈ 𝔽(I+i)
11. I ⊆ I+i+j
12. K : fset(ℕ)
13. J : fset(ℕ)
14. g : J ⟶ K
15. f : I+i+j,s(fl-join(I+i;s(phi);(i=0)))(K)
16. ¬((f i) = 0 ∈ Point(dM(K)))
17. f ∈ K ⟶ I+i+j
18. (((phi)<s>)<s>)<f> = 1 ∈ Point(face_lattice(K))
19. (s(phi) m(i;j) ⋅ f) = 1
20. (f ⋅ g i) = 0 ∈ Point(dM(J))
21. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
22. (i0) ⋅ s ⋅ s ⋅ f ⋅ g = m(i;j) ⋅ f ⋅ g ∈ J ⟶ I+i
⊢ (((phi)<s ⋅ s>)<f>)<g> = 1 ∈ Point(face_lattice(J))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  I  :  fset(\mBbbN{})
4.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
5.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\} 
6.  rho  :  Gamma(I+i)
7.  phi  :  \mBbbF{}(I)
8.  u  :  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
9.  a0  :  cubical-path-0(Gamma;A;I;i;rho;phi;u)
10.  (i=0)  \mmember{}  \mBbbF{}(I+i)
11.  I  \msubseteq{}  I+i+j
12.  K  :  fset(\mBbbN{})
13.  J  :  fset(\mBbbN{})
14.  g  :  J  {}\mrightarrow{}  K
15.  f  :  I+i+j,s(fl-join(I+i;s(phi);(i=0)))(K)
16.  \mneg{}((f  i)  =  0)
17.  f  \mmember{}  K  {}\mrightarrow{}  I+i+j
18.  (((phi)<s>)<s>)<f>  =  1
19.  (s(phi)  m(i;j)  \mcdot{}  f)  =  1
20.  (f  \mcdot{}  g  i)  =  0
21.  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:I,phi(J).    ((a0  (i0)(rho)  f)  =  u((i0)  \mcdot{}  f))
22.  (i0)  \mcdot{}  s  \mcdot{}  s  \mcdot{}  f  \mcdot{}  g  =  m(i;j)  \mcdot{}  f  \mcdot{}  g
\mvdash{}  (phi)<s  \mcdot{}  s  \mcdot{}  f  \mcdot{}  g>  =  1


By

---

Latex:
RepeatFor  2  ((RWO  "fl-morph-comp2<"  0  THENA  Auto))

---

Home Index