---

Step * 1 1 2 2 1 2 1 2 1 2 1 1 2 1 2 1 1 1 1 1 1 3 1 2 2 2 of Lemma pi-comp-uniformity

.....subterm..... T:t
2:n
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 ⊢ _}
27. <rho> o iota o subset-trans(I+i;K+k;g ⋅ f,i=k;s(phi)) = <g ⋅ f,i=k(rho)> o iota ∈ K+k,(s(phi))<g ⋅ f,i=k> j⟶ Gamma
28. z : K+k,(s(phi))<g ⋅ f,i=k> j⟶ Gamma
⊢ K+k,(s(phi))<g ⋅ f,i=k> ⊢ ((A)<g ⋅ f,i=k(rho)>)iota
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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
27.  <rho>  o  iota  o  subset-trans(I+i;K+k;g  \mcdot{}  f,i=k;s(phi))  =  <g  \mcdot{}  f,i=k(rho)>  o  iota
28.  z  :  K+k,(s(phi))<g  \mcdot{}  f,i=k>  j{}\mrightarrow{}  Gamma
\mvdash{}  K+k,(s(phi))<g  \mcdot{}  f,i=k>  \mvdash{}  ((A)<g  \mcdot{}  f,i=k(rho)>)iota


By

---

Latex:
Auto

---

Home Index