Step
*
1
1
2
2
1
2
1
2
1
2
1
1
2
1
2
1
1
1
1
1
1
3
of Lemma
pi-comp-uniformity
.....aux.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. I : fset(ℕ)
7. J : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. j : {j:ℕ| ¬j ∈ J}
10. g : J ⟶ I
11. rho : Gamma(I+i)
12. phi : 𝔽(I)
13. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
14. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
15. K : fset(ℕ)
16. f : K ⟶ J
17. u : A(f(g((i1)(rho))))
18. k : {i:ℕ| ¬i ∈ K}
19. g ⋅ f,i=1-k = g,i=j ⋅ f,j=1-k ∈ K+k ⟶ I+i
20. xx : A(g ⋅ f,i=k(rho))
21. K+k,(s(phi))<g ⋅ f,i=k> ⊢ ∈ 𝕌{[i' | j']}
22. K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ij⊢
23. K+k,(s(phi))<g ⋅ f,i=k> ⊢ (B)<(g ⋅ f,i=k(rho);xx)> o iota
24. <rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)) o p ∈ K+k,(s(phi))
<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ij⟶ Gamma
25. p ∈ K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ij⟶ K+k,(s(phi))<g ⋅ f,i=k>
26. (A)<rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)) o p
= ((A)<rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)))p
∈ {K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ⊢ _}
⊢ (((A)<g ⋅ f,i=k(rho)>)iota)p
= ((A)<rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)))p
∈ {K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ⊢ _}
BY
{ ((Subst' iota ~ subset_iota((s(phi))<g ⋅ f,i=k>) 0 THENA (RepUR ``subset-iota subset_iota`` 0 THEN Auto))
THEN EqCDA
THEN (Subst' subset_iota((s(phi))<g ⋅ f,i=k>) ~ iota 0 THENA (RepUR ``subset-iota subset_iota`` 0 THEN Auto))) }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. I : fset(ℕ)
7. J : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. j : {j:ℕ| ¬j ∈ J}
10. g : J ⟶ I
11. rho : Gamma(I+i)
12. phi : 𝔽(I)
13. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
14. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
15. K : fset(ℕ)
16. f : K ⟶ J
17. u : A(f(g((i1)(rho))))
18. k : {i:ℕ| ¬i ∈ K}
19. g ⋅ f,i=1-k = g,i=j ⋅ f,j=1-k ∈ K+k ⟶ I+i
20. xx : A(g ⋅ f,i=k(rho))
21. K+k,(s(phi))<g ⋅ f,i=k> ⊢ ∈ 𝕌{[i' | j']}
22. K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ij⊢
23. K+k,(s(phi))<g ⋅ f,i=k> ⊢ (B)<(g ⋅ f,i=k(rho);xx)> o iota
24. <rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)) o p ∈ K+k,(s(phi))
<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ij⟶ Gamma
25. p ∈ K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ij⟶ K+k,(s(phi))<g ⋅ f,i=k>
26. (A)<rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)) o p
= ((A)<rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)))p
∈ {K+k,(s(phi))<g ⋅ f,i=k>.((A)<g ⋅ f,i=k(rho)>)iota ⊢ _}
⊢ ((A)<g ⋅ f,i=k(rho)>)iota = (A)<rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)) ∈ {K+k,(s(phi))<g ⋅ f,i=k> ⊢ _}
Latex:
Latex:
.....aux.....
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. I : fset(\mBbbN{})
7. J : fset(\mBbbN{})
8. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\}
9. j : \{j:\mBbbN{}| \mneg{}j \mmember{} J\}
10. g : J {}\mrightarrow{} I
11. rho : Gamma(I+i)
12. phi : \mBbbF{}(I)
13. mu : \{I+i,s(phi) \mvdash{} \_:(\mPi{}A B)<rho> o iota\}
14. lambda : cubical-path-0(Gamma;\mPi{}A B;I;i;rho;phi;mu)
15. K : fset(\mBbbN{})
16. f : K {}\mrightarrow{} J
17. u : A(f(g((i1)(rho))))
18. k : \{i:\mBbbN{}| \mneg{}i \mmember{} K\}
19. g \mcdot{} f,i=1-k = g,i=j \mcdot{} f,j=1-k
20. xx : A(g \mcdot{} f,i=k(rho))
21. K+k,(s(phi))<g \mcdot{} f,i=k> \mvdash{} \mmember{} \mBbbU{}\{[i' | j']\}
22. K+k,(s(phi))<g \mcdot{} f,i=k>.((A)<g \mcdot{} f,i=k(rho)>)iota ij\mvdash{}
23. K+k,(s(phi))<g \mcdot{} f,i=k> \mvdash{} (B)<(g \mcdot{} f,i=k(rho);xx)> o iota
24. <rho> o iota o subset-trans(I+i;K+k;g \mcdot{} f,i=k;s(phi)) o p
\mmember{} K+k,(s(phi))<g \mcdot{} f,i=k>.((A)<g \mcdot{} f,i=k(rho)>)iota ij{}\mrightarrow{} Gamma
25. p \mmember{} K+k,(s(phi))<g \mcdot{} f,i=k>.((A)<g \mcdot{} f,i=k(rho)>)iota ij{}\mrightarrow{} K+k,(s(phi))<g \mcdot{} f,i=k>
26. (A)<rho> o iota o subset-trans(I+i;K+k;g \mcdot{} f,i=k;s(phi)) o p
= ((A)<rho> o iota o subset-trans(I+i;K+k;g \mcdot{} f,i=k;s(phi)))p
\mvdash{} (((A)<g \mcdot{} f,i=k(rho)>)iota)p = ((A)<rho> o iota o subset-trans(I+i;K+k;g \mcdot{} f,i=k;s(phi)))p
By
Latex:
((Subst' iota \msim{} subset\_iota((s(phi))<g \mcdot{} f,i=k>) 0
THENA (RepUR ``subset-iota subset\_iota`` 0 THEN Auto)
)
THEN EqCDA
THEN (Subst' subset\_iota((s(phi))<g \mcdot{} f,i=k>) \msim{} iota 0
THENA (RepUR ``subset-iota subset\_iota`` 0 THEN Auto)
))
Home
Index