Step
*
1
of Lemma
pi-comp_wf3
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. pi-comp(Gamma;A;B;cA;cB) ∈ I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ mu:{I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
⟶ lambda:cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ u1:A(f((i1)(rho)))
⟶ B((f((i1)(rho));u1))
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
12. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
13. J : fset(ℕ)
14. K : fset(ℕ)
15. f : J ⟶ I
16. g : K ⟶ J
17. u : A(f((i1)(rho)))
⊢ (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda J f u (f((i1)(rho));u) g)
= (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g (u f((i1)(rho)) g))
∈ B(g((f((i1)(rho));u)))
BY
{ Assert ⌜∀j:ℕ. ((¬j ∈ J) ⇒ ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) f,i=j(rho) (j1)) = u ∈ A((j1)(f,i=j(rho)))))⌝⋅ }
1
.....assertion.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. pi-comp(Gamma;A;B;cA;cB) ∈ I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ mu:{I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
⟶ lambda:cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ u1:A(f((i1)(rho)))
⟶ B((f((i1)(rho));u1))
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
12. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
13. J : fset(ℕ)
14. K : fset(ℕ)
15. f : J ⟶ I
16. g : K ⟶ J
17. u : A(f((i1)(rho)))
⊢ ∀j:ℕ. ((¬j ∈ J) ⇒ ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) f,i=j(rho) (j1)) = u ∈ A((j1)(f,i=j(rho)))))
2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. pi-comp(Gamma;A;B;cA;cB) ∈ I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ mu:{I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
⟶ lambda:cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ u1:A(f((i1)(rho)))
⟶ B((f((i1)(rho));u1))
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
12. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
13. J : fset(ℕ)
14. K : fset(ℕ)
15. f : J ⟶ I
16. g : K ⟶ J
17. u : A(f((i1)(rho)))
18. ∀j:ℕ. ((¬j ∈ J) ⇒ ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) f,i=j(rho) (j1)) = u ∈ A((j1)(f,i=j(rho)))))
⊢ (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda J f u (f((i1)(rho));u) g)
= (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g (u f((i1)(rho)) g))
∈ B(g((f((i1)(rho));u)))
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. B : \{Gamma.A \mvdash{} \_\}
4. cA : Gamma \mvdash{} CompOp(A)
5. cB : Gamma.A \mvdash{} CompOp(B)
6. pi-comp(Gamma;A;B;cA;cB) \mmember{} I:fset(\mBbbN{})
{}\mrightarrow{} i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\}
{}\mrightarrow{} rho:Gamma(I+i)
{}\mrightarrow{} phi:\mBbbF{}(I)
{}\mrightarrow{} mu:\{I+i,s(phi) \mvdash{} \_:(\mPi{}A B)<rho> o iota\}
{}\mrightarrow{} lambda:cubical-path-0(Gamma;\mPi{}A B;I;i;rho;phi;mu)
{}\mrightarrow{} J:fset(\mBbbN{})
{}\mrightarrow{} f:J {}\mrightarrow{} I
{}\mrightarrow{} u1:A(f((i1)(rho)))
{}\mrightarrow{} B((f((i1)(rho));u1))
7. I : fset(\mBbbN{})
8. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\}
9. rho : Gamma(I+i)
10. phi : \mBbbF{}(I)
11. mu : \{I+i,s(phi) \mvdash{} \_:(\mPi{}A B)<rho> o iota\}
12. lambda : cubical-path-0(Gamma;\mPi{}A B;I;i;rho;phi;mu)
13. J : fset(\mBbbN{})
14. K : fset(\mBbbN{})
15. f : J {}\mrightarrow{} I
16. g : K {}\mrightarrow{} J
17. u : A(f((i1)(rho)))
\mvdash{} (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda J f u (f((i1)(rho));u) g)
= (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f \mcdot{} g (u f((i1)(rho)) g))
By
Latex:
Assert \mkleeneopen{}\mforall{}j:\mBbbN{}. ((\mneg{}j \mmember{} J) {}\mRightarrow{} ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) f,i=j(rho) (j1)) = u))\mkleeneclose{}\mcdot{}
Home
Index