Step
*
1
2
1
3
1
2
1
1
1
2
1
2
3
1
of Lemma
pi-comp_wf3
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. 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)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma.A(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}. ∀a0:cubical-path-0(Gamma.A;B;I;i;rho;phi;u).
((cB I i rho phi u a0 (i1)(rho) g)
= (cB J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ B(g((i1)(rho))))
7. 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))
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 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
14. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
15. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
16. J : fset(ℕ)
17. K : fset(ℕ)
18. f : J ⟶ I
19. g : K ⟶ J
20. u : A(f((i1)(rho)))
21. ∀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)))))
22. j : ℕ
23. ¬j ∈ J
24. k : ℕ
25. ¬k ∈ K
26. pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
= pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
∈ B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
27. cubical-path-condition(Gamma.A;B;K;k;(f ⋅ g,i=k(rho);
pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;
(u f((i1)(rho)) g);k));f ⋅ g(phi);pi-comp-app(Gamma;A;I;i;rho;phi;
mu;K;f ⋅ g;k;
...);...)
28. ∀u:A(f((i0)(rho)))
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
29. (lambda J f
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0)) (f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0))) g)
= (lambda K f ⋅ g ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)) f((i0)(rho)) g))
∈ B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
30. B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
= B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
∈ Type
31. B(g((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)))))
= B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
∈ Type
⊢ B((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0))))
= B((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j))))
∈ Type
BY
{ ((RWW "cc-adjoin-cube-restriction" 0 THENA Auto) THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }
1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. 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)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma.A(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}. ∀a0:cubical-path-0(Gamma.A;B;I;i;rho;phi;u).
((cB I i rho phi u a0 (i1)(rho) g)
= (cB J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ B(g((i1)(rho))))
7. 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))
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 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
14. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
15. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
16. J : fset(ℕ)
17. K : fset(ℕ)
18. f : J ⟶ I
19. g : K ⟶ J
20. u : A(f((i1)(rho)))
21. ∀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)))))
22. j : ℕ
23. ¬j ∈ J
24. k : ℕ
25. ¬k ∈ K
26. pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
= pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
∈ B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
27. cubical-path-condition(Gamma.A;B;K;k;(f ⋅ g,i=k(rho);
pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;
(u f((i1)(rho)) g);k));f ⋅ g(phi);pi-comp-app(Gamma;A;I;i;rho;phi;
mu;K;f ⋅ g;k;
...);...)
28. ∀u:A(f((i0)(rho)))
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
29. (lambda J f
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0)) (f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0))) g)
= (lambda K f ⋅ g ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)) f((i0)(rho)) g))
∈ B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
30. B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
= B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
∈ Type
31. B(g((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)))))
= B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
∈ Type
⊢ Gamma ij⊢
2
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. 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)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma.A(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}. ∀a0:cubical-path-0(Gamma.A;B;I;i;rho;phi;u).
((cB I i rho phi u a0 (i1)(rho) g)
= (cB J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ B(g((i1)(rho))))
7. 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))
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 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
14. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
15. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
16. J : fset(ℕ)
17. K : fset(ℕ)
18. f : J ⟶ I
19. g : K ⟶ J
20. u : A(f((i1)(rho)))
21. ∀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)))))
22. j : ℕ
23. ¬j ∈ J
24. k : ℕ
25. ¬k ∈ K
26. pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
= pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
∈ B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
27. cubical-path-condition(Gamma.A;B;K;k;(f ⋅ g,i=k(rho);
pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;
(u f((i1)(rho)) g);k));f ⋅ g(phi);pi-comp-app(Gamma;A;I;i;rho;phi;
mu;K;f ⋅ g;k;
...);...)
28. ∀u:A(f((i0)(rho)))
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
29. (lambda J f
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0)) (f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0))) g)
= (lambda K f ⋅ g ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)) f((i0)(rho)) g))
∈ B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
30. B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
= B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
∈ Type
31. B(g((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)))))
= B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
∈ Type
⊢ cubical-type{[i | j]:l}(Gamma)A
3
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. 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)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma.A(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}. ∀a0:cubical-path-0(Gamma.A;B;I;i;rho;phi;u).
((cB I i rho phi u a0 (i1)(rho) g)
= (cB J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ B(g((i1)(rho))))
7. 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))
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 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
14. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
15. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
16. J : fset(ℕ)
17. K : fset(ℕ)
18. f : J ⟶ I
19. g : K ⟶ J
20. u : A(f((i1)(rho)))
21. ∀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)))))
22. j : ℕ
23. ¬j ∈ J
24. k : ℕ
25. ¬k ∈ K
26. pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
= pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
∈ B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
27. cubical-path-condition(Gamma.A;B;K;k;(f ⋅ g,i=k(rho);
pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;
(u f((i1)(rho)) g);k));f ⋅ g(phi);pi-comp-app(Gamma;A;I;i;rho;phi;
mu;K;f ⋅ g;k;
...);...)
28. ∀u:A(f((i0)(rho)))
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
29. (lambda J f
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0)) (f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0))) g)
= (lambda K f ⋅ g ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)) f((i0)(rho)) g))
∈ B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
30. B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
= B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
∈ Type
31. B(g((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)))))
= B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
∈ Type
⊢ f((i0)(rho)) = (j0)(f,i=j(rho)) ∈ Gamma(J)
4
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. 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)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma.A(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}. ∀a0:cubical-path-0(Gamma.A;B;I;i;rho;phi;u).
((cB I i rho phi u a0 (i1)(rho) g)
= (cB J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ B(g((i1)(rho))))
7. 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))
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 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
14. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
15. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
16. J : fset(ℕ)
17. K : fset(ℕ)
18. f : J ⟶ I
19. g : K ⟶ J
20. u : A(f((i1)(rho)))
21. ∀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)))))
22. j : ℕ
23. ¬j ∈ J
24. k : ℕ
25. ¬k ∈ K
26. pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
= pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))
∈ B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
27. cubical-path-condition(Gamma.A;B;K;k;(f ⋅ g,i=k(rho);
pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;
(u f((i1)(rho)) g);k));f ⋅ g(phi);pi-comp-app(Gamma;A;I;i;rho;phi;
mu;K;f ⋅ g;k;
...);...)
28. ∀u:A(f((i0)(rho)))
((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
29. (lambda J f
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0)) (f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r_j(f,i=1-j(rho)) (j0))) g)
= (lambda K f ⋅ g ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)) f((i0)(rho)) g))
∈ B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
30. B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
= B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0)))))
∈ Type
31. B(g((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)))))
= B((k0)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k))))
∈ Type
⊢ (pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r_j(f,i=1-j(rho)) (j0))
= (pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) f,i=j(rho) (j0))
∈ A(f((i0)(rho)))
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. B : \{Gamma.A \mvdash{} \_\}
4. cA : Gamma \mvdash{} CompOp(A)
5. 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)
6. \mforall{}I,J:fset(\mBbbN{}). \mforall{}i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\} . \mforall{}j:\{j:\mBbbN{}| \mneg{}j \mmember{} J\} . \mforall{}g:J {}\mrightarrow{} I. \mforall{}rho:Gamma.A(I+i). \mforall{}phi:\mBbbF{}(I).
\mforall{}u:\{I+i,s(phi) \mvdash{} \_:(B)<rho> o iota\}. \mforall{}a0:cubical-path-0(Gamma.A;B;I;i;rho;phi;u).
((cB I i rho phi u a0 (i1)(rho) g)
= (cB J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g)))
7. 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))
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{} \_:(\mPi{}A B)<rho> o iota\}
13. lambda : J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} u:A(f((i0)(rho))) {}\mrightarrow{} B((f((i0)(rho));u))
14. \mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:A(f((i0)(rho))).
((lambda J f u (f((i0)(rho));u) g) = (lambda K f \mcdot{} g (u f((i0)(rho)) g)))
15. cubical-path-condition(Gamma;\mPi{}A B;I;i;rho;phi;mu;lambda)
16. J : fset(\mBbbN{})
17. K : fset(\mBbbN{})
18. f : J {}\mrightarrow{} I
19. g : K {}\mrightarrow{} J
20. u : A(f((i1)(rho)))
21. \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))
22. j : \mBbbN{}
23. \mneg{}j \mmember{} J
24. k : \mBbbN{}
25. \mneg{}k \mmember{} K
26. pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f \mcdot{} g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;
(u f((i1)(rho)) g);k))
= pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;f \mcdot{} g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;
(u f((i1)(rho)) g);k))
27. cubical-path-condition(Gamma.A;B;K;k;(f \mcdot{} g,i=k(rho);
pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;
(u f((i1)(rho)) g);k));f \mcdot{} g(phi);...;...)
28. \mforall{}u:A(f((i0)(rho))). ((lambda J f u (f((i0)(rho));u) g) = (lambda K f \mcdot{} g (u f((i0)(rho)) g)))
29. (lambda J f
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r\_j(f,i=1-j(rho)) (j0)) (f((i0)(rho));
(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;
u;j) r\_j(f,i=1-j(rho)) (j0))) g)
= (lambda K f \mcdot{} g ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r\_j(f,i=1-j(rho)) (j0)) f((i0)(rho)) g))
30. B((k0)((f \mcdot{} g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;(u f((i1)(rho)) g);k))))
= B(g((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r\_j(f,i=1-j(rho)) (j0)))))
31. B(g((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)))))
= B((k0)((f \mcdot{} g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;(u f((i1)(rho)) g);k))))
\mvdash{} B((f((i0)(rho));(pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) r\_j(f,i=1-j(rho)) (j0))))
= B((j0)((f,i=j(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j))))
By
Latex:
((RWW "cc-adjoin-cube-restriction" 0 THENA Auto) THEN RepeatFor 2 ((EqCD THEN Try (Trivial))))
Home
Index