---

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. a1 : A((i1)(rho))
9. I,phi ⊢
10. J : fset(ℕ)
11. f : I,phi(J)
12. (f ∈ J ⟶ I) ∧ (phi f) = 1
⊢ (a1 (i1)(rho) f) = u((i1) ⋅ f) ∈ A(f((i1)(rho))) ∈ ℙ'
BY
{ ((Assert (phi s ⋅ (i1) ⋅ f) = 1 BY
          (RWW "nh-comp-assoc s-comp-nc-1" 0 THEN Auto))
   THEN (Assert (s(phi) (i1) ⋅ f) = 1 BY
               (RWO "name-morph-satisfies-comp" 0 THEN Auto))
   THEN (Assert (i1) ⋅ f ∈ I+i,s(phi)(J) BY
               (BLemma `member-cubical-subset-I_cube` THEN Auto))
   THEN (InstLemma `cubical-term-at_wf` [⌜I+i,s(phi)⌝;⌜(A)<rho> o iota⌝;⌜u⌝;⌜J⌝;⌜(i1) ⋅ 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. a1 : A((i1)(rho))
9. I,phi ⊢
10. J : fset(ℕ)
11. f : I,phi(J)
12. (f ∈ J ⟶ I) ∧ (phi f) = 1
13. (phi s ⋅ (i1) ⋅ f) = 1
14. (s(phi) (i1) ⋅ f) = 1
15. (i1) ⋅ f ∈ I+i,s(phi)(J)
16. u((i1) ⋅ f) ∈ (A)<rho> o iota((i1) ⋅ f)
⊢ (a1 (i1)(rho) f) = u((i1) ⋅ f) ∈ A(f((i1)(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.  a1  :  A((i1)(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{}  (a1  (i1)(rho)  f)  =  u((i1)  \mcdot{}  f)  \mmember{}  \mBbbP{}'


By

---

Latex:
((Assert  (phi  s  \mcdot{}  (i1)  \mcdot{}  f)  =  1  BY
                (RWW  "nh-comp-assoc  s-comp-nc-1"  0  THEN  Auto))
  THEN  (Assert  (s(phi)  (i1)  \mcdot{}  f)  =  1  BY
                          (RWO  "name-morph-satisfies-comp"  0  THEN  Auto))
  THEN  (Assert  (i1)  \mcdot{}  f  \mmember{}  I+i,s(phi)(J)  BY
                          (BLemma  `member-cubical-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{}(i1)  \mcdot{}  f\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index