---

Step * 1 of Lemma sigmacomp_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
5. composition-uniformity(Gamma;A;cA)
6. cB : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma.A(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}
⟶ cubical-path-0(Gamma.A;B;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma.A;B;I;i;rho;phi;u)
7. composition-uniformity(Gamma.A;B;cB)
8. I : fset(ℕ)
9. J : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. j : {j:ℕ| ¬j ∈ J} 
12. g : J ⟶ I
13. rho : Gamma(I+i)
14. phi : 𝔽(I)
15. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
16. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
17. fillA : filling-op(Gamma;A)
⊢ (let v = fillA I i rho phi mu.1 (fst(lambda)) in
    let w = cB I i (rho;v) phi mu.2 (snd(lambda)) in
    <(v rho (i1)), w> (i1)(rho) g)
= let v = fillA J j g,i=j(rho) g(phi) (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).1 (fst((lambda (i0)(rho) g))) in
   let w = cB J j (g,i=j(rho);v) g(phi) (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).2 (snd((lambda (i0)(rho) g))) in
   <(v g,i=j(rho) (j1)), w>
∈ Σ A B(g((i1)(rho)))
BY
{ Assert ⌜mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}⌝⋅ }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
5. composition-uniformity(Gamma;A;cA)
6. cB : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma.A(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}
⟶ cubical-path-0(Gamma.A;B;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma.A;B;I;i;rho;phi;u)
7. composition-uniformity(Gamma.A;B;cB)
8. I : fset(ℕ)
9. J : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. j : {j:ℕ| ¬j ∈ J} 
12. g : J ⟶ I
13. rho : Gamma(I+i)
14. phi : 𝔽(I)
15. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
16. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
17. fillA : filling-op(Gamma;A)
⊢ mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
5. composition-uniformity(Gamma;A;cA)
6. cB : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma.A(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}
⟶ cubical-path-0(Gamma.A;B;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma.A;B;I;i;rho;phi;u)
7. composition-uniformity(Gamma.A;B;cB)
8. I : fset(ℕ)
9. J : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. j : {j:ℕ| ¬j ∈ J} 
12. g : J ⟶ I
13. rho : Gamma(I+i)
14. phi : 𝔽(I)
15. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
16. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
17. fillA : filling-op(Gamma;A)
18. mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}
⊢ (let v = fillA I i rho phi mu.1 (fst(lambda)) in
    let w = cB I i (rho;v) phi mu.2 (snd(lambda)) in
    <(v rho (i1)), w> (i1)(rho) g)
= let v = fillA J j g,i=j(rho) g(phi) (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).1 (fst((lambda (i0)(rho) g))) in
   let w = cB J j (g,i=j(rho);v) g(phi) (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).2 (snd((lambda (i0)(rho) g))) in
   <(v g,i=j(rho) (j1)), w>
∈ Σ A B(g((i1)(rho)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  B  :  \{Gamma.A  \mvdash{}  \_\}
4.  cA  :  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{}  cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{}  cubical-path-1(Gamma;A;I;i;rho;phi;u)
5.  composition-uniformity(Gamma;A;cA)
6.  cB  :  I:fset(\mBbbN{})
{}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
{}\mrightarrow{}  rho:Gamma.A(I+i)
{}\mrightarrow{}  phi:\mBbbF{}(I)
{}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(B)<rho>  o  iota\}
{}\mrightarrow{}  cubical-path-0(Gamma.A;B;I;i;rho;phi;u)
{}\mrightarrow{}  cubical-path-1(Gamma.A;B;I;i;rho;phi;u)
7.  composition-uniformity(Gamma.A;B;cB)
8.  I  :  fset(\mBbbN{})
9.  J  :  fset(\mBbbN{})
10.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
11.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\} 
12.  g  :  J  {}\mrightarrow{}  I
13.  rho  :  Gamma(I+i)
14.  phi  :  \mBbbF{}(I)
15.  mu  :  \{I+i,s(phi)  \mvdash{}  \_:(\mSigma{}  A  B)<rho>  o  iota\}
16.  lambda  :  cubical-path-0(Gamma;\mSigma{}  A  B;I;i;rho;phi;mu)
17.  fillA  :  filling-op(Gamma;A)
\mvdash{}  (let  v  =  fillA  I  i  rho  phi  mu.1  (fst(lambda))  in
        let  w  =  cB  I  i  (rho;v)  phi  mu.2  (snd(lambda))  in
        <(v  rho  (i1)),  w>  (i1)(rho)  g)
=  let  v  =  fillA  J  j  g,i=j(rho)  g(phi)  (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).1 
                    (fst((lambda  (i0)(rho)  g)))  in
      let  w  =  cB  J  j  (g,i=j(rho);v)  g(phi)  (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).2 
                      (snd((lambda  (i0)(rho)  g)))  in
      <(v  g,i=j(rho)  (j1)),  w>


By

---

Latex:
Assert  \mkleeneopen{}mu.1  \mmember{}  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}\mkleeneclose{}\mcdot{}

---

Home Index