---

Step * 1 1 1 1 2 1 1 1 1 1 of Lemma discrete-comp_wf


1. G : CubicalSet{j}
2. T : Type
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. rho : G(I+i)
6. phi : 𝔽(I)
7. u : {I+i,s(phi) ⊢ _:discr(T)}
8. a0 : T
9. ∀J:fset(ℕ). ∀f:I,phi(J).  (a0 = u((i0) ⋅ f) ∈ T)
10. J : fset(ℕ)
11. ∀f:I,phi(J). (a0 = u((i0) ⋅ f) ∈ T)
12. f : J ⟶ I
13. (phi f) = 1
14. a0 = u((i0) ⋅ f) ∈ T
15. fs : fset({p:fset(names(I)) × fset(names(I))| ↑fset-disjoint(NamesDeq;fst(p);snd(p))} )
16. phi = \/(λpr.irr_face(I;fst(pr);snd(pr))"(fs)) ∈ Point(face_lattice(I))
⊢ u((i1) ⋅ f) = u((i0) ⋅ f) ∈ T
BY
{ (DupHyp (-4) THEN (RWO  "-2" (-1) THENA Auto)) }

1
1. G : CubicalSet{j}
2. T : Type
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. rho : G(I+i)
6. phi : 𝔽(I)
7. u : {I+i,s(phi) ⊢ _:discr(T)}
8. a0 : T
9. ∀J:fset(ℕ). ∀f:I,phi(J).  (a0 = u((i0) ⋅ f) ∈ T)
10. J : fset(ℕ)
11. ∀f:I,phi(J). (a0 = u((i0) ⋅ f) ∈ T)
12. f : J ⟶ I
13. (phi f) = 1
14. a0 = u((i0) ⋅ f) ∈ T
15. fs : fset({p:fset(names(I)) × fset(names(I))| ↑fset-disjoint(NamesDeq;fst(p);snd(p))} )
16. phi = \/(λpr.irr_face(I;fst(pr);snd(pr))"(fs)) ∈ Point(face_lattice(I))
17. (\/(λpr.irr_face(I;fst(pr);snd(pr))"(fs)) f) = 1
⊢ u((i1) ⋅ f) = u((i0) ⋅ f) ∈ T

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  T  :  Type
3.  I  :  fset(\mBbbN{})
4.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
5.  rho  :  G(I+i)
6.  phi  :  \mBbbF{}(I)
7.  u  :  \{I+i,s(phi)  \mvdash{}  \_:discr(T)\}
8.  a0  :  T
9.  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:I,phi(J).    (a0  =  u((i0)  \mcdot{}  f))
10.  J  :  fset(\mBbbN{})
11.  \mforall{}f:I,phi(J).  (a0  =  u((i0)  \mcdot{}  f))
12.  f  :  J  {}\mrightarrow{}  I
13.  (phi  f)  =  1
14.  a0  =  u((i0)  \mcdot{}  f)
15.  fs  :  fset(\{p:fset(names(I))  \mtimes{}  fset(names(I))|  \muparrow{}fset-disjoint(NamesDeq;fst(p);snd(p))\}  )
16.  phi  =  \mbackslash{}/(\mlambda{}pr.irr\_face(I;fst(pr);snd(pr))"(fs))
\mvdash{}  u((i1)  \mcdot{}  f)  =  u((i0)  \mcdot{}  f)


By

---

Latex:
(DupHyp  (-4)  THEN  (RWO    "-2"  (-1)  THENA  Auto))

---

Home Index