Proof of Nuprl Lemma : csm-composition

Step * 2 1 1 1 2 1 2 2 1 1 1 2 of Lemma csm-composition_wf

1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. 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)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
6. λI,i,rho. (comp I i (sigma)rho) ∈ I:fset(ℕ)
   ⟶ i:{i:ℕ| ¬i ∈ I}
   ⟶ rho:Delta(I+i)
   ⟶ phi:𝔽(I)
   ⟶ u:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
   ⟶ cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
   ⟶ cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u)
7. I : fset(ℕ)
8. J : fset(ℕ)
9. i : {i:ℕ| ¬i ∈ I}
10. j : {j:ℕ| ¬j ∈ J}
11. g : J ⟶ I

12. ∀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 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((i1)(rho))))
13. rho : Delta(I+i)
14. phi : 𝔽(I)
15. ∀u:{I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u).
      ((comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
      = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
      ∈ A(g((i1)((sigma)rho))))

16. {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}

17. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
18. ∀a0:cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)
      ((comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
      = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
      ∈ A(g((i1)((sigma)rho))))
19. a0 : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
20. (comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
= (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
∈ A(g((i1)((sigma)rho)))
21. (A)sigma(g((i1)(rho))) = A(g((i1)((sigma)rho))) ∈ Type
22. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) ∈ {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
23. v : {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
24. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) = v ∈ {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
25. v1 : rho:Gamma(J+j)
⟶ phi:𝔽(J)
⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
⟶ {a1:A((j1)(rho))| cubical-path-condition'(Gamma;A;J;j;rho;phi;u;a1)}
26. (comp J j)
= v1
∈ (rho:Gamma(J+j)
  ⟶ phi:𝔽(J)
  ⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
  ⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
  ⟶ cubical-path-1(Gamma;A;J;j;rho;phi;u))
27. F : rho:Gamma(J+j)
⟶ phi:𝔽(J)
⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
⟶ A((j1)(rho))
28. v1
= F
∈ (rho:Gamma(J+j)
  ⟶ phi:𝔽(J)
  ⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
  ⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
  ⟶ A((j1)(rho)))
⊢ (F (sigma)g,i=j(rho) g(phi) v (a0 (i0)(rho) g))
= (F g,i=j((sigma)rho) g(phi) v (a0 (i0)((sigma)rho) g))
∈ A(g((i1)((sigma)rho)))
BY
{ SubsumeC ⌜A((j1)((sigma)g,i=j(rho)))⌝⋅ }

1
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. 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)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
6. λI,i,rho. (comp I i (sigma)rho) ∈ I:fset(ℕ)
   ⟶ i:{i:ℕ| ¬i ∈ I}
   ⟶ rho:Delta(I+i)
   ⟶ phi:𝔽(I)
   ⟶ u:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
   ⟶ cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
   ⟶ cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u)
7. I : fset(ℕ)
8. J : fset(ℕ)
9. i : {i:ℕ| ¬i ∈ I}
10. j : {j:ℕ| ¬j ∈ J}
11. g : J ⟶ I

12. ∀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).

16. {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}

17. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
18. ∀a0:cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)
      ((comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
      = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
      ∈ A(g((i1)((sigma)rho))))
19. a0 : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
20. (comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
= (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
∈ A(g((i1)((sigma)rho)))
21. (A)sigma(g((i1)(rho))) = A(g((i1)((sigma)rho))) ∈ Type
22. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) ∈ {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
23. v : {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
24. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) = v ∈ {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
25. v1 : rho:Gamma(J+j)
⟶ phi:𝔽(J)
⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
⟶ {a1:A((j1)(rho))| cubical-path-condition'(Gamma;A;J;j;rho;phi;u;a1)}
26. (comp J j)
= v1
∈ (rho:Gamma(J+j)
  ⟶ phi:𝔽(J)
  ⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
  ⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
  ⟶ cubical-path-1(Gamma;A;J;j;rho;phi;u))
27. F : rho:Gamma(J+j)
⟶ phi:𝔽(J)
⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
⟶ A((j1)(rho))
28. v1
= F
∈ (rho:Gamma(J+j)
  ⟶ phi:𝔽(J)
  ⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
  ⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
  ⟶ A((j1)(rho)))
⊢ (F (sigma)g,i=j(rho) g(phi) v (a0 (i0)(rho) g))
= (F g,i=j((sigma)rho) g(phi) v (a0 (i0)((sigma)rho) g))
∈ A((j1)((sigma)g,i=j(rho)))

2
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. 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)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
6. λI,i,rho. (comp I i (sigma)rho) ∈ I:fset(ℕ)
   ⟶ i:{i:ℕ| ¬i ∈ I}
   ⟶ rho:Delta(I+i)
   ⟶ phi:𝔽(I)
   ⟶ u:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
   ⟶ cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
   ⟶ cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u)
7. I : fset(ℕ)
8. J : fset(ℕ)
9. i : {i:ℕ| ¬i ∈ I}
10. j : {j:ℕ| ¬j ∈ J}
11. g : J ⟶ I

12. ∀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).

16. {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}

17. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
18. ∀a0:cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)
      ((comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
      = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
      ∈ A(g((i1)((sigma)rho))))
19. a0 : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
20. (comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g)
= (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))
∈ A(g((i1)((sigma)rho)))
21. (A)sigma(g((i1)(rho))) = A(g((i1)((sigma)rho))) ∈ Type
22. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) ∈ {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
23. v : {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
24. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) = v ∈ {J+j,s(g(phi)) ⊢ _:(A)<(sigma)g,i=j(rho)> o iota}
25. v1 : rho:Gamma(J+j)
⟶ phi:𝔽(J)
⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
⟶ {a1:A((j1)(rho))| cubical-path-condition'(Gamma;A;J;j;rho;phi;u;a1)}
26. (comp J j)
= v1
∈ (rho:Gamma(J+j)
  ⟶ phi:𝔽(J)
  ⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
  ⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
  ⟶ cubical-path-1(Gamma;A;J;j;rho;phi;u))
27. F : rho:Gamma(J+j)
⟶ phi:𝔽(J)
⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
⟶ A((j1)(rho))
28. v1
= F
∈ (rho:Gamma(J+j)
  ⟶ phi:𝔽(J)
  ⟶ u:{J+j,s(phi) ⊢ _:(A)<rho> o iota}
  ⟶ cubical-path-0(Gamma;A;J;j;rho;phi;u)
  ⟶ A((j1)(rho)))
29. (F (sigma)g,i=j(rho) g(phi) v (a0 (i0)(rho) g))
= (F g,i=j((sigma)rho) g(phi) v (a0 (i0)((sigma)rho) g))
∈ A((j1)((sigma)g,i=j(rho)))
⊢ A((j1)((sigma)g,i=j(rho))) ⊆r A(g((i1)((sigma)rho)))

Latex:

Latex:
1. Gamma : CubicalSet\{j\} 2. Delta : CubicalSet\{j\} 3. sigma : Delta j{}\mrightarrow{} Gamma 4. A : \{Gamma \mvdash{} \_\} 5. 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{} cubical-path-1(Gamma;A;I;i;rho;phi;u) 6. \mlambda{}I,i,rho. (comp I i (sigma)rho) \mmember{} I:fset(\mBbbN{}) {}\mrightarrow{} i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\} {}\mrightarrow{} rho:Delta(I+i) {}\mrightarrow{} phi:\mBbbF{}(I) {}\mrightarrow{} u:\{I+i,s(phi) \mvdash{} \_:((A)sigma)<rho> o iota\} {}\mrightarrow{} cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u) {}\mrightarrow{} cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u) 7. I : fset(\mBbbN{}) 8. J : fset(\mBbbN{}) 9. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\} 10. j : \{j:\mBbbN{}| \mneg{}j \mmember{} J\} 11. g : J {}\mrightarrow{} I 12. \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 J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))) 13. rho : Delta(I+i) 14. phi : \mBbbF{}(I) 15. \mforall{}u:\{I+i,s(phi) \mvdash{} \_:(A)<(sigma)rho> o iota\}. \mforall{}a0:cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u). ((comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g) = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))) 16. \{I+i,s(phi) \mvdash{} \_:((A)sigma)<rho> o iota\} = \{I+i,s(phi) \mvdash{} \_:(A)<(sigma)rho> o iota\} 17. u : \{I+i,s(phi) \mvdash{} \_:((A)sigma)<rho> o iota\} 18. \mforall{}a0:cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u) ((comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g) = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g))) 19. a0 : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u) 20. (comp I i (sigma)rho phi u a0 (i1)((sigma)rho) g) = (comp J j g,i=j((sigma)rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)((sigma)rho) g)) 21. (A)sigma(g((i1)(rho))) = A(g((i1)((sigma)rho))) 22. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) \mmember{} \{J+j,s(g(phi)) \mvdash{} \_:(A)<(sigma)g,i=j(rho)> o iota\} 23. v : \{J+j,s(g(phi)) \mvdash{} \_:(A)<(sigma)g,i=j(rho)> o iota\} 24. (u)subset-trans(I+i;J+j;g,i=j;s(phi)) = v 25. v1 : rho:Gamma(J+j) {}\mrightarrow{} phi:\mBbbF{}(J) {}\mrightarrow{} u:\{J+j,s(phi) \mvdash{} \_:(A)<rho> o iota\} {}\mrightarrow{} cubical-path-0(Gamma;A;J;j;rho;phi;u) {}\mrightarrow{} \{a1:A((j1)(rho))| cubical-path-condition'(Gamma;A;J;j;rho;phi;u;a1)\} 26. (comp J j) = v1 27. F : rho:Gamma(J+j) {}\mrightarrow{} phi:\mBbbF{}(J) {}\mrightarrow{} u:\{J+j,s(phi) \mvdash{} \_:(A)<rho> o iota\} {}\mrightarrow{} cubical-path-0(Gamma;A;J;j;rho;phi;u) {}\mrightarrow{} A((j1)(rho)) 28. v1 = F \mvdash{} (F (sigma)g,i=j(rho) g(phi) v (a0 (i0)(rho) g)) = (F g,i=j((sigma)rho) g(phi) v (a0 (i0)((sigma)rho) g)) By Latex: SubsumeC \mkleeneopen{}A((j1)((sigma)g,i=j(rho)))\mkleeneclose{}\mcdot{} Home Index