Proof of Nuprl Lemma : pi-comp-nu-uniformity

Step * 1 2 3 2 1 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)))
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))
23. A(r_k(f ⋅ g,i=1-k(rho))) = A(f ⋅ g,i=k(rho)) ∈ Type
⊢ (fill K k f ⋅ g,i=1-k(rho) 0 () (u f((i1)(rho)) g))
= (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:A(f ⋅ g,i=1-k(rho))|

   (section-iota(Gamma;A;K+k;f ⋅ g,i=1-k(rho);a) = () ∈ {K+k,s(0) ⊢ _:(A)<f ⋅ g,i=1-k(rho)> o iota})

∧ ((a f ⋅ g,i=1-k(rho) (k0)) = (u f((i1)(rho)) g) ∈ A((k0)(f ⋅ g,i=1-k(rho))))}
BY
{ (RepeatFor 2 (EqCD) THEN Auto) }

1
.....subterm..... T:t
1:n
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).

= (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))
23. A(r_k(f ⋅ g,i=1-k(rho))) = A(f ⋅ g,i=k(rho)) ∈ Type
⊢ (fill K k f ⋅ g,i=1-k(rho) 0)
= (fill K k g,j=k(f,i=1-j(rho)) g(0))
∈ (u:{K+k,s(0) ⊢ _:(A)<f ⋅ g,i=1-k(rho)> o iota}
⟶ a0:cubical-path-0(Gamma;A;K;k;f ⋅ g,i=1-k(rho);0;u)
⟶ {a:A(f ⋅ g,i=1-k(rho))|

      (section-iota(Gamma;A;K+k;f ⋅ g,i=1-k(rho);a) = u ∈ {K+k,s(0) ⊢ _:(A)<f ⋅ g,i=1-k(rho)> o iota})

∧ ((a f ⋅ g,i=1-k(rho) (k0)) = a0 ∈ A((k0)(f ⋅ g,i=1-k(rho))))} )

2
.....subterm..... T:t
2:n
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).

= (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))
23. A(r_k(f ⋅ g,i=1-k(rho))) = A(f ⋅ g,i=k(rho)) ∈ Type
⊢ () = (())subset-trans(J+j;K+k;g,j=k;s(0)) ∈ {K+k,s(0) ⊢ _:(A)<f ⋅ g,i=1-k(rho)> o iota}

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)) 22. ((fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k) f \mcdot{} 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 \mcdot{} g,i=1-k(rho) r\_k) 23. A(r\_k(f \mcdot{} g,i=1-k(rho))) = A(f \mcdot{} g,i=k(rho)) \mvdash{} (fill K k f \mcdot{} g,i=1-k(rho) 0 () (u f((i1)(rho)) g)) = (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)) By Latex: (RepeatFor 2 (EqCD) THEN Auto) Home Index