Proof of Nuprl Lemma : composition-op-nc-e

Step * 1 2 3 1 2 2 2 1 1 2 of Lemma composition-op-nc-e

1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
4. composition-uniformity(Gamma;A;comp)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ I}
8. ∀g: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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : A((i0)(rho))
13. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
14. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
15. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
16. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
17. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
18. A((i0)(rho)) = A((j0)(e(i;j)(rho))) ∈ Type
19. J : fset(ℕ)
20. ∀f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
21. f : I,phi(J)
22. (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
23. (j0)(e(i;j)(rho)) = (i0)(rho) ∈ Gamma(I)
⊢ (a0 (j0)(e(i;j)(rho)) f) = (u)subset-trans(I+i;I+j;e(i;j);s(phi))((j0) ⋅ f) ∈ A(f((j0)(e(i;j)(rho))))
BY
{ ((CubicalSubsetICube (-3) THENA Auto) THEN NthHypEqGen (-4) THEN EqCD) }

1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
4. composition-uniformity(Gamma;A;comp)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ I}
8. ∀g: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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : A((i0)(rho))
13. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
14. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
15. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
16. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
17. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
18. A((i0)(rho)) = A((j0)(e(i;j)(rho))) ∈ Type
19. J : fset(ℕ)
20. ∀f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
21. f : I,phi(J)
22. (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
23. (j0)(e(i;j)(rho)) = (i0)(rho) ∈ Gamma(I)
24. f ∈ J ⟶ I
25. (phi f) = 1
⊢ A(f((i0)(rho))) = A(f((i0)(rho))) ∈ Type

2
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
4. composition-uniformity(Gamma;A;comp)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ I}
8. ∀g: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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : A((i0)(rho))
13. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
14. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
15. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
16. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
17. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
18. A((i0)(rho)) = A((j0)(e(i;j)(rho))) ∈ Type
19. J : fset(ℕ)
20. ∀f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
21. f : I,phi(J)
22. (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
23. (j0)(e(i;j)(rho)) = (i0)(rho) ∈ Gamma(I)
24. f ∈ J ⟶ I
25. (phi f) = 1
⊢ (a0 (j0)(e(i;j)(rho)) f) = (a0 (i0)(rho) f) ∈ A(f((i0)(rho)))

3
.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
4. composition-uniformity(Gamma;A;comp)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ I}
8. ∀g: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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : A((i0)(rho))
13. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
14. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
15. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
16. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
17. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
18. A((i0)(rho)) = A((j0)(e(i;j)(rho))) ∈ Type
19. J : fset(ℕ)
20. ∀f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
21. f : I,phi(J)
22. (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
23. (j0)(e(i;j)(rho)) = (i0)(rho) ∈ Gamma(I)
24. f ∈ J ⟶ I
25. (phi f) = 1
⊢ (u)subset-trans(I+i;I+j;e(i;j);s(phi))((j0) ⋅ f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))

4
.....antecedent.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
4. composition-uniformity(Gamma;A;comp)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ I}
8. ∀g: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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : A((i0)(rho))
13. ∀J:fset(ℕ). ∀f:I,phi(J).  ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
14. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
15. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
16. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
17. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
18. A((i0)(rho)) = A((j0)(e(i;j)(rho))) ∈ Type
19. J : fset(ℕ)
20. ∀f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
21. f : I,phi(J)
22. (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
23. (j0)(e(i;j)(rho)) = (i0)(rho) ∈ Gamma(I)
24. f ∈ J ⟶ I
25. (phi f) = 1
⊢ True

Latex:

Latex:
1. Gamma : CubicalSet\{j\} 2. A : \{Gamma \mvdash{} \_\} 3. comp : 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{} cubical-path-0(Gamma;A;I;i;rho;phi;u) {}\mrightarrow{} \{a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)\} 4. composition-uniformity(Gamma;A;comp) 5. I : fset(\mBbbN{}) 6. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\} 7. j : \{j:\mBbbN{}| \mneg{}j \mmember{} I\} 8. \mforall{}g:I {}\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). ((comp I i rho phi u a0 (i1)(rho) g) = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))) 9. rho : Gamma(I+i) 10. phi : \mBbbF{}(I) 11. u : \{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\} 12. a0 : A((i0)(rho)) 13. \mforall{}J:fset(\mBbbN{}). \mforall{}f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) \mcdot{} f)) 14. (comp I i rho phi u a0 (i1)(rho) 1) = (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1)) 15. A((i1)(rho)) = A((j1)(e(i;j)(rho))) 16. comp I i rho phi u a0 \mmember{} \{a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)\} 17. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) \mmember{} \{I+j,s(1(phi)) \mvdash{} \_:(A)<e(i;j)(rho)> o iota\} 18. A((i0)(rho)) = A((j0)(e(i;j)(rho))) 19. J : fset(\mBbbN{}) 20. \mforall{}f:I,phi(J). ((a0 (i0)(rho) f) = u((i0) \mcdot{} f)) 21. f : I,phi(J) 22. (a0 (i0)(rho) f) = u((i0) \mcdot{} f) 23. (j0)(e(i;j)(rho)) = (i0)(rho) \mvdash{} (a0 (j0)(e(i;j)(rho)) f) = (u)subset-trans(I+i;I+j;e(i;j);s(phi))((j0) \mcdot{} f) By Latex: ((CubicalSubsetICube (-3) THENA Auto) THEN NthHypEqGen (-4) THEN EqCD) Home Index