---

Step * 1 2 2 1 2 of Lemma sigmacomp_wf1


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. i : {i:ℕ| ¬i ∈ I} 
10. rho : Gamma(I+i)
11. phi : 𝔽(I)
12. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
13. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
14. fillA : filling-op(Gamma;A)
15. mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}
16. fst(lambda) ∈ cubical-path-0(Gamma;A;I;i;rho;phi;mu.1)
17. v : {a:A(rho)| 
         (section-iota(Gamma;A;I+i;rho;a) = mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota})
         ∧ ((a rho (i0)) = (fst(lambda)) ∈ A((i0)(rho)))} 
18. mu.2 ∈ {I+i,s(phi) ⊢ _:(B)<(rho;v)> o iota}
⊢ <(v rho (i1)), cB I i (rho;v) phi mu.2 (snd(lambda))> ∈ cubical-path-1(Gamma;Σ A B;I;i;rho;phi;mu)
BY
{ Assert ⌜snd(lambda) ∈ cubical-path-0(Gamma.A;B;I;i;(rho;v);phi;mu.2)⌝⋅ }

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. i : {i:ℕ| ¬i ∈ I} 
10. rho : Gamma(I+i)
11. phi : 𝔽(I)
12. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
13. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
14. fillA : filling-op(Gamma;A)
15. mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}
16. fst(lambda) ∈ cubical-path-0(Gamma;A;I;i;rho;phi;mu.1)
17. v : {a:A(rho)| 
         (section-iota(Gamma;A;I+i;rho;a) = mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota})
         ∧ ((a rho (i0)) = (fst(lambda)) ∈ A((i0)(rho)))} 
18. mu.2 ∈ {I+i,s(phi) ⊢ _:(B)<(rho;v)> o iota}
⊢ snd(lambda) ∈ cubical-path-0(Gamma.A;B;I;i;(rho;v);phi;mu.2)

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. i : {i:ℕ| ¬i ∈ I} 
10. rho : Gamma(I+i)
11. phi : 𝔽(I)
12. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
13. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
14. fillA : filling-op(Gamma;A)
15. mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}
16. fst(lambda) ∈ cubical-path-0(Gamma;A;I;i;rho;phi;mu.1)
17. v : {a:A(rho)| 
         (section-iota(Gamma;A;I+i;rho;a) = mu.1 ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota})
         ∧ ((a rho (i0)) = (fst(lambda)) ∈ A((i0)(rho)))} 
18. mu.2 ∈ {I+i,s(phi) ⊢ _:(B)<(rho;v)> o iota}
19. snd(lambda) ∈ cubical-path-0(Gamma.A;B;I;i;(rho;v);phi;mu.2)
⊢ <(v rho (i1)), cB I i (rho;v) phi mu.2 (snd(lambda))> ∈ cubical-path-1(Gamma;Σ A B;I;i;rho;phi;mu)

---

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.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
10.  rho  :  Gamma(I+i)
11.  phi  :  \mBbbF{}(I)
12.  mu  :  \{I+i,s(phi)  \mvdash{}  \_:(\mSigma{}  A  B)<rho>  o  iota\}
13.  lambda  :  cubical-path-0(Gamma;\mSigma{}  A  B;I;i;rho;phi;mu)
14.  fillA  :  filling-op(Gamma;A)
15.  mu.1  \mmember{}  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
16.  fst(lambda)  \mmember{}  cubical-path-0(Gamma;A;I;i;rho;phi;mu.1)
17.  v  :  \{a:A(rho)|  (section-iota(Gamma;A;I+i;rho;a)  =  mu.1)  \mwedge{}  ((a  rho  (i0))  =  (fst(lambda)))\} 
18.  mu.2  \mmember{}  \{I+i,s(phi)  \mvdash{}  \_:(B)<(rho;v)>  o  iota\}
\mvdash{}  <(v  rho  (i1)),  cB  I  i  (rho;v)  phi  mu.2  (snd(lambda))>  \mmember{}  cubical-path-1(Gamma;\mSigma{}  A  B;I;i;rho;phi;mu)


By

---

Latex:
Assert  \mkleeneopen{}snd(lambda)  \mmember{}  cubical-path-0(Gamma.A;B;I;i;(rho;v);phi;mu.2)\mkleeneclose{}\mcdot{}

---

Home Index