Step
*
1
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)
⊢ 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> ∈ cubical-path-1(Gamma;Σ A B;I;i;rho;phi;mu)
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. 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)
⊢ 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. 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}
⊢ 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> ∈ 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)
\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> \mmember{} cubical-path-1(Gamma;\mSigma{} A B;I;i;rho;phi;mu)
By
Latex:
Assert \mkleeneopen{}mu.1 \mmember{} \{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}\mkleeneclose{}\mcdot{}
Home
Index