---

Step * 1 of Lemma cubical-path-condition_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. rho : Gamma(I+i)
6. phi : 𝔽(I)
7. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
8. a0 : A((i0)(rho))
9. I,phi ⊢
10. J : fset(ℕ)
11. f : I,phi(J)
12. (f ∈ J ⟶ I) ∧ (phi f) = 1
⊢ (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))) ∈ ℙ'
BY
{ ((Assert (i0) ⋅ f ∈ I+i,s(phi)(J) BY
          ((BLemma comp-nc-0-subset-I_cube) THEN Auto))
   THEN (InstLemma `cubical-term-at_wf` [⌜I+i,s(phi)⌝;⌜(A)<rho> o iota⌝;⌜u⌝;⌜J⌝;⌜(i0) ⋅ f⌝]⋅ THENA Auto)
   ) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. rho : Gamma(I+i)
6. phi : 𝔽(I)
7. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
8. a0 : A((i0)(rho))
9. I,phi ⊢
10. J : fset(ℕ)
11. f : I,phi(J)
12. (f ∈ J ⟶ I) ∧ (phi f) = 1
13. (i0) ⋅ f ∈ I+i,s(phi)(J)
14. u((i0) ⋅ f) ∈ (A)<rho> o iota((i0) ⋅ f)
⊢ (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))) ∈ ℙ'

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  I  :  fset(\mBbbN{})
4.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
5.  rho  :  Gamma(I+i)
6.  phi  :  \mBbbF{}(I)
7.  u  :  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
8.  a0  :  A((i0)(rho))
9.  I,phi  \mvdash{}
10.  J  :  fset(\mBbbN{})
11.  f  :  I,phi(J)
12.  (f  \mmember{}  J  {}\mrightarrow{}  I)  \mwedge{}  (phi  f)  =  1
\mvdash{}  (a0  (i0)(rho)  f)  =  u((i0)  \mcdot{}  f)  \mmember{}  \mBbbP{}'


By

---

Latex:
((Assert  (i0)  \mcdot{}  f  \mmember{}  I+i,s(phi)(J)  BY
                ((BLemma  comp-nc-0-subset-I\_cube)  THEN  Auto))
  THEN  (InstLemma  `cubical-term-at\_wf`  [\mkleeneopen{}I+i,s(phi)\mkleeneclose{};\mkleeneopen{}(A)<rho>  o  iota\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}(i0)  \mcdot{}  f\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  )

---

Home Index