---

Step * 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)
⊢ ((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
{ (Assert u1 ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;()) BY
         (MemTypeCD
          THEN Auto
          THEN D 0
          THEN Auto
          THEN (CubicalSubsetICube (-1) THENA Auto)
          THEN Unfold `name-morph-satisfies` -1
          THEN (RWO "fl-morph-0" (-1) THENA Auto)
          THEN (Assert ⌜False⌝⋅ THEN Auto)
          THEN MoveToConcl (-1)
          THEN Fold `not` 0
          THEN 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;())
⊢ ((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)))

---

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)
\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:
(Assert  u1  \mmember{}  cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())  BY
              (MemTypeCD
                THEN  Auto
                THEN  D  0
                THEN  Auto
                THEN  (CubicalSubsetICube  (-1)  THENA  Auto)
                THEN  Unfold  `name-morph-satisfies`  -1
                THEN  (RWO  "fl-morph-0"  (-1)  THENA  Auto)
                THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                THEN  MoveToConcl  (-1)
                THEN  Fold  `not`  0
                THEN  Auto))

---

Home Index