Step
*
1
of Lemma
pi-comp-uniformity
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}
⊢ let nu = pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k) in
cB K k (g ⋅ f,i=k(rho);nu) g ⋅ f(phi) pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;nu)
pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;g ⋅ f;k;nu)
= let nu = pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k) in
cB K k (f,j=k(g,i=j(rho));nu) f(g(phi))
pi-comp-app(Gamma;A;J;j;g,i=j(rho);g(phi);(mu)subset-trans(I+i;J+j;g,i=j;s(phi));K;f;k;nu)
pi-comp-lambda(Gamma;A;J;j;g,i=j(rho);λK,g@0. (lambda K g ⋅ g@0);K;f;k;nu)
∈ B((f(g((i1)(rho)));u))
BY
{ (RepUR ``let`` 0
THEN SubsumeC ⌜cubical-path-1(Gamma.A;B;K;k;(g ⋅ f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k));g ⋅ f(phi);
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;
pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)))⌝⋅
) }
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}
⊢ (cB K k (g ⋅ f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)) g ⋅ f(phi)
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k))
pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)))
= (cB K k (f,j=k(g,i=j(rho));pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k)) f(g(phi))
pi-comp-app(Gamma;A;J;j;g,i=j(rho);g(phi);(mu)subset-trans(I+i;J+j;g,i=j;s(phi));K;f;k;
pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k))
pi-comp-lambda(Gamma;A;J;j;g,i=j(rho);λK,g@0. (lambda K g ⋅ g@0);K;f;k;pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k))\000C)
∈ cubical-path-1(Gamma.A;B;K;k;(g ⋅ f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k));g ⋅ f(phi);
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)))
2
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. (cB K k (g ⋅ f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)) g ⋅ f(phi)
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k))
pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)))
= (cB K k (f,j=k(g,i=j(rho));pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k)) f(g(phi))
pi-comp-app(Gamma;A;J;j;g,i=j(rho);g(phi);(mu)subset-trans(I+i;J+j;g,i=j;s(phi));K;f;k;
pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k))
pi-comp-lambda(Gamma;A;J;j;g,i=j(rho);λK,g@0. (lambda K g ⋅ g@0);K;f;k;pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k))\000C)
∈ cubical-path-1(Gamma.A;B;K;k;(g ⋅ f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k));g ⋅ f(phi);
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)))
⊢ cubical-path-1(Gamma.A;B;K;k;(g ⋅ f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k));g ⋅ f(phi);
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k)))
⊆r B((f(g((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. 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\}
\mvdash{} let nu = pi-comp-nu(Gamma;A;cA;I;i;rho;K;g \mcdot{} f;u;k) in
cB K k (g \mcdot{} f,i=k(rho);nu) g \mcdot{} f(phi) pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g \mcdot{} f;k;nu)
pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;g \mcdot{} f;k;nu)
= let nu = pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k) in
cB K k (f,j=k(g,i=j(rho));nu) f(g(phi))
pi-comp-app(Gamma;A;J;j;g,i=j(rho);g(phi);(mu)subset-trans(I+i;J+j;g,i=j;s(phi));K;f;k;nu)
pi-comp-lambda(Gamma;A;J;j;g,i=j(rho);\mlambda{}K,g@0. (lambda K g \mcdot{} g@0);K;f;k;nu)
By
Latex:
(RepUR ``let`` 0
THEN SubsumeC \mkleeneopen{}cubical-path-1(Gamma.A;B;K;k;(g \mcdot{} f,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;g \mcdot{} f;
u;k));g \mcdot{} f(phi);
pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g \mcdot{} f;k;
pi-comp-nu(Gamma;A;cA;I;i;rho;K;g \mcdot{} f;u;k)))\mkleeneclose{}\mcdot{}
)
Home
Index