Step
*
1
of Lemma
pi-comp-nu-uniformity
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : ℕ
6. ¬i ∈ I
7. rho : Gamma(I+i)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. u : A(f((i1)(rho)))
13. j : ℕ
14. ¬j ∈ J
15. k : ℕ
16. ¬k ∈ K
17. fill : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a:A(rho)|
(section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))}
18. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((fill I i rho phi u a0 rho g,i=j)
= (fill J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g,i=j(rho)))
19. u ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
20. fill J j f,i=1-j(rho) 0 () u ∈ A(f,i=1-j(rho))
21. (fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k)
= (fill K k g,j=k(f,i=1-j(rho)) g(0) (())subset-trans(J+j;K+k;g,j=k;s(0)) (u (j0)(f,i=1-j(rho)) g))
∈ A(g,j=k(f,i=1-j(rho)))
⊢ ((fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) r_j) f,i=j(rho) g,j=k)
= (fill K k f ⋅ g,i=1-k(rho) 0 () (u f((i1)(rho)) g) f ⋅ g,i=1-k(rho) r_k)
∈ A(f ⋅ g,i=k(rho))
BY
{ ApFunToHypEquands `Z' ⌜(Z f ⋅ g,i=1-k(rho) r_k)⌝ ⌜A(f ⋅ g,i=k(rho))⌝ (-1)⋅ }
1
.....fun wf.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : ℕ
6. ¬i ∈ I
7. rho : Gamma(I+i)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. u : A(f((i1)(rho)))
13. j : ℕ
14. ¬j ∈ J
15. k : ℕ
16. ¬k ∈ K
17. fill : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a:A(rho)|
(section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))}
18. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((fill I i rho phi u a0 rho g,i=j)
= (fill J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g,i=j(rho)))
19. u ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
20. fill J j f,i=1-j(rho) 0 () u ∈ A(f,i=1-j(rho))
21. (fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k)
= (fill K k g,j=k(f,i=1-j(rho)) g(0) (())subset-trans(J+j;K+k;g,j=k;s(0)) (u (j0)(f,i=1-j(rho)) g))
∈ A(g,j=k(f,i=1-j(rho)))
22. Z : A(g,j=k(f,i=1-j(rho)))
⊢ (Z f ⋅ g,i=1-k(rho) r_k) = (Z f ⋅ g,i=1-k(rho) r_k) ∈ A(f ⋅ g,i=k(rho))
2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : ℕ
6. ¬i ∈ I
7. rho : Gamma(I+i)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. u : A(f((i1)(rho)))
13. j : ℕ
14. ¬j ∈ J
15. k : ℕ
16. ¬k ∈ K
17. fill : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a:A(rho)|
(section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))}
18. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((fill I i rho phi u a0 rho g,i=j)
= (fill J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g,i=j(rho)))
19. u ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
20. fill J j f,i=1-j(rho) 0 () u ∈ A(f,i=1-j(rho))
21. (fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k)
= (fill K k g,j=k(f,i=1-j(rho)) g(0) (())subset-trans(J+j;K+k;g,j=k;s(0)) (u (j0)(f,i=1-j(rho)) g))
∈ A(g,j=k(f,i=1-j(rho)))
22. ((fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k) f ⋅ g,i=1-k(rho) r_k)
= (fill K k g,j=k(f,i=1-j(rho)) g(0) (())subset-trans(J+j;K+k;g,j=k;s(0)) (u (j0)(f,i=1-j(rho)) g) f ⋅ g,i=1-k(rho) r_k)
∈ A(f ⋅ g,i=k(rho))
⊢ ((fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) r_j) f,i=j(rho) g,j=k)
= (fill K k f ⋅ g,i=1-k(rho) 0 () (u f((i1)(rho)) g) f ⋅ g,i=1-k(rho) r_k)
∈ A(f ⋅ g,i=k(rho))
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. cA : Gamma \mvdash{} CompOp(A)
4. I : fset(\mBbbN{})
5. i : \mBbbN{}
6. \mneg{}i \mmember{} I
7. rho : Gamma(I+i)
8. J : fset(\mBbbN{})
9. K : fset(\mBbbN{})
10. f : J {}\mrightarrow{} I
11. g : K {}\mrightarrow{} J
12. u : A(f((i1)(rho)))
13. j : \mBbbN{}
14. \mneg{}j \mmember{} J
15. k : \mBbbN{}
16. \mneg{}k \mmember{} K
17. fill : I:fset(\mBbbN{})
{}\mrightarrow{} i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\}
{}\mrightarrow{} rho:Gamma(I+i)
{}\mrightarrow{} phi:\mBbbF{}(I)
{}\mrightarrow{} u:\{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}
{}\mrightarrow{} a0:cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{} \{a:A(rho)| (section-iota(Gamma;A;I+i;rho;a) = u) \mwedge{} ((a rho (i0)) = a0)\}
18. \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(I+i). \mforall{}phi:\mBbbF{}(I).
\mforall{}u:\{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}. \mforall{}a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((fill I i rho phi u a0 rho g,i=j)
= (fill J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g)))
19. u \mmember{} cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
20. fill J j f,i=1-j(rho) 0 () u \mmember{} A(f,i=1-j(rho))
21. (fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k)
= (fill K k g,j=k(f,i=1-j(rho)) g(0) (())subset-trans(J+j;K+k;g,j=k;s(0)) (u (j0)(f,i=1-j(rho)) g))
\mvdash{} ((fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) r\_j) f,i=j(rho) g,j=k)
= (fill K k f \mcdot{} g,i=1-k(rho) 0 () (u f((i1)(rho)) g) f \mcdot{} g,i=1-k(rho) r\_k)
By
Latex:
ApFunToHypEquands `Z' \mkleeneopen{}(Z f \mcdot{} g,i=1-k(rho) r\_k)\mkleeneclose{} \mkleeneopen{}A(f \mcdot{} g,i=k(rho))\mkleeneclose{} (-1)\mcdot{}
Home
Index