---

Step * 1 1 of Lemma pi-comp-nu-property


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. J : fset(ℕ)
8. f : J ⟶ I
9. u1 : A(f((i1)(rho)))
10. j : {j:ℕ| ¬j ∈ J} 
11. fill : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a:A(rho)| 
    (section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))} 
12. filling-uniformity(Gamma;A;fill)
13. u1 ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
⊢ ((fill J j f,i=1-j(rho) 0 () u1 f,i=1-j(rho) r_j) f,i=j(rho) (j1)) = u1 ∈ A((j1)(f,i=j(rho)))
BY
{ (GenConclTerm ⌜fill J j f,i=1-j(rho) 0 () u1⌝⋅ THENA Auto) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. J : fset(ℕ)
8. f : J ⟶ I
9. u1 : A(f((i1)(rho)))
10. j : {j:ℕ| ¬j ∈ J} 
11. fill : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a:A(rho)| 
    (section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))} 
12. filling-uniformity(Gamma;A;fill)
13. u1 ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
14. v : {a:A(f,i=1-j(rho))| 
         (section-iota(Gamma;A;J+j;f,i=1-j(rho);a) = () ∈ {J+j,s(0) ⊢ _:(A)<f,i=1-j(rho)> o iota})
         ∧ ((a f,i=1-j(rho) (j0)) = u1 ∈ A((j0)(f,i=1-j(rho))))} 
15. (fill J j f,i=1-j(rho) 0 () u1)
= v
∈ {a:A(f,i=1-j(rho))| 
   (section-iota(Gamma;A;J+j;f,i=1-j(rho);a) = () ∈ {J+j,s(0) ⊢ _:(A)<f,i=1-j(rho)> o iota})
   ∧ ((a f,i=1-j(rho) (j0)) = u1 ∈ A((j0)(f,i=1-j(rho))))} 
⊢ ((v f,i=1-j(rho) r_j) f,i=j(rho) (j1)) = u1 ∈ A((j1)(f,i=j(rho)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  Gamma  \mvdash{}  CompOp(A)
4.  I  :  fset(\mBbbN{})
5.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
6.  rho  :  Gamma(I+i)
7.  J  :  fset(\mBbbN{})
8.  f  :  J  {}\mrightarrow{}  I
9.  u1  :  A(f((i1)(rho)))
10.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\} 
11.  fill  :  I:fset(\mBbbN{})
{}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
{}\mrightarrow{}  rho:Gamma(I+i)
{}\mrightarrow{}  phi:\mBbbF{}(I)
{}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
{}\mrightarrow{}  a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{}  \{a:A(rho)|  (section-iota(Gamma;A;I+i;rho;a)  =  u)  \mwedge{}  ((a  rho  (i0))  =  a0)\} 
12.  filling-uniformity(Gamma;A;fill)
13.  u1  \mmember{}  cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
\mvdash{}  ((fill  J  j  f,i=1-j(rho)  0  ()  u1  f,i=1-j(rho)  r\_j)  f,i=j(rho)  (j1))  =  u1


By

---

Latex:
(GenConclTerm  \mkleeneopen{}fill  J  j  f,i=1-j(rho)  0  ()  u1\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index