Proof of Nuprl Lemma : pi-comp-property

Step * 1 1 1 3 3 1 1 2 1 1 1 2 1 1 1 1 2 1 of Lemma pi-comp-property

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. composition-uniformity(Gamma.A;B;cB)
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : I@0:fset(ℕ) ⟶ a:I+i,s(phi)(I@0) ⟶ (ΠA B)<rho> o iota(a)

12. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I+i,s(phi)(I@0).  ((mu I@0 a a f) = (mu J f(a)) ∈ (ΠA B)<rho> o iota(f(a)))

13. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
14. J : fset(ℕ)
15. f : J ⟶ I
16. (phi f) = 1
17. K : fset(ℕ)
18. g : K ⟶ J
19. u : A(g(f((i1)(rho))))
20. k : ℕ
21. ¬k ∈ K
22. v : B((k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))))
23. ∀J@0:fset(ℕ). ∀f@0:{f1:J@0 ⟶ K| (f ⋅ g(phi) f1) = 1} .
((v (k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))) f@0)

      = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))((k1) ⋅ f@0)

∈ B(f@0((k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))))))
24. (v (k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))) 1)
= pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))((k1) ⋅ 1)
∈ B(1((k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k)))))
25. (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k) f ⋅ g,i=k(rho) (k1)) = u ∈ A((k1)(f ⋅ g,i=k(rho)))
26. A((k1)(f ⋅ g,i=k(rho))) = A(g(f((i1)(rho)))) ∈ Type
27. (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k) f ⋅ g,i=k(rho) (k1) ⋅ 1) = u ∈ A(g(f((i1)(rho))))
28. (i1) ⋅ f ∈ I+i,s(phi)(J)
29. (λK@0,g@0. (mu J (i1) ⋅ f K@0 g ⋅ g@0))
= (mu K (i1) ⋅ f ⋅ g)

∈ (J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ K ⟶ u:A(f@0(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((f@0(<rho> K (i1) ⋅ f ⋅ g);u)))

30. f ⋅ g,i=k ⋅ (k1) ⋅ 1 = (i1) ⋅ f ⋅ g ∈ K ⟶ I+i

31. (mu J (i1) ⋅ f K g ⋅ 1) = (mu K (i1) ⋅ f ⋅ g K 1) ∈ (u:A(1(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((1(<rho> K (i1) ⋅ f ⋅ g);u)))

32. A(1(<rho> K (i1) ⋅ f ⋅ g)) = A(g(f((i1)(rho)))) ∈ Type

33. (mu J (i1) ⋅ f K g ⋅ 1 u) = (mu K (i1) ⋅ f ⋅ g K 1 u) ∈ B((1(<rho> K (i1) ⋅ f ⋅ g);u))

⊢ (mu J (i1) ⋅ f K g u)

= (mu K f ⋅ g,i=k ⋅ (k1) ⋅ 1 K 1 (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k) f ⋅ g,i=k(rho) (k1) ⋅ 1))

∈ B((g(f((i1)(rho)));u))
BY
{ (NthHypEqGen (-1) THEN 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. composition-uniformity(Gamma.A;B;cB)
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : I@0:fset(ℕ) ⟶ a:I+i,s(phi)(I@0) ⟶ (ΠA B)<rho> o iota(a)

12. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I+i,s(phi)(I@0).  ((mu I@0 a a f) = (mu J f(a)) ∈ (ΠA B)<rho> o iota(f(a)))

      = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))((k1) ⋅ f@0)

∈ (J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ K ⟶ u:A(f@0(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((f@0(<rho> K (i1) ⋅ f ⋅ g);u)))

30. f ⋅ g,i=k ⋅ (k1) ⋅ 1 = (i1) ⋅ f ⋅ g ∈ K ⟶ I+i

31. (mu J (i1) ⋅ f K g ⋅ 1) = (mu K (i1) ⋅ f ⋅ g K 1) ∈ (u:A(1(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((1(<rho> K (i1) ⋅ f ⋅ g);u)))

32. A(1(<rho> K (i1) ⋅ f ⋅ g)) = A(g(f((i1)(rho)))) ∈ Type

33. (mu J (i1) ⋅ f K g ⋅ 1 u) = (mu K (i1) ⋅ f ⋅ g K 1 u) ∈ B((1(<rho> K (i1) ⋅ f ⋅ g);u))

⊢ B((g(f((i1)(rho)));u)) = B((1(<rho> K (i1) ⋅ f ⋅ g);u)) ∈ Type

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. composition-uniformity(Gamma.A;B;cB)
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : I@0:fset(ℕ) ⟶ a:I+i,s(phi)(I@0) ⟶ (ΠA B)<rho> o iota(a)

12. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I+i,s(phi)(I@0).  ((mu I@0 a a f) = (mu J f(a)) ∈ (ΠA B)<rho> o iota(f(a)))

      = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))((k1) ⋅ f@0)

∈ (J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ K ⟶ u:A(f@0(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((f@0(<rho> K (i1) ⋅ f ⋅ g);u)))

30. f ⋅ g,i=k ⋅ (k1) ⋅ 1 = (i1) ⋅ f ⋅ g ∈ K ⟶ I+i

31. (mu J (i1) ⋅ f K g ⋅ 1) = (mu K (i1) ⋅ f ⋅ g K 1) ∈ (u:A(1(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((1(<rho> K (i1) ⋅ f ⋅ g);u)))

32. A(1(<rho> K (i1) ⋅ f ⋅ g)) = A(g(f((i1)(rho)))) ∈ Type

33. (mu J (i1) ⋅ f K g ⋅ 1 u) = (mu K (i1) ⋅ f ⋅ g K 1 u) ∈ B((1(<rho> K (i1) ⋅ f ⋅ g);u))

⊢ (mu J (i1) ⋅ f K g u) = (mu J (i1) ⋅ f K g ⋅ 1 u) ∈ B((g(f((i1)(rho)));u))

3
.....subterm..... T:t
3: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. composition-uniformity(Gamma.A;B;cB)
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. mu : I@0:fset(ℕ) ⟶ a:I+i,s(phi)(I@0) ⟶ (ΠA B)<rho> o iota(a)

12. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I+i,s(phi)(I@0).  ((mu I@0 a a f) = (mu J f(a)) ∈ (ΠA B)<rho> o iota(f(a)))

      = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))((k1) ⋅ f@0)

∈ (J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ K ⟶ u:A(f@0(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((f@0(<rho> K (i1) ⋅ f ⋅ g);u)))

30. f ⋅ g,i=k ⋅ (k1) ⋅ 1 = (i1) ⋅ f ⋅ g ∈ K ⟶ I+i

31. (mu J (i1) ⋅ f K g ⋅ 1) = (mu K (i1) ⋅ f ⋅ g K 1) ∈ (u:A(1(<rho> K (i1) ⋅ f ⋅ g)) ⟶ B((1(<rho> K (i1) ⋅ f ⋅ g);u)))

32. A(1(<rho> K (i1) ⋅ f ⋅ g)) = A(g(f((i1)(rho)))) ∈ Type

33. (mu J (i1) ⋅ f K g ⋅ 1 u) = (mu K (i1) ⋅ f ⋅ g K 1 u) ∈ B((1(<rho> K (i1) ⋅ f ⋅ g);u))

⊢ (mu K f ⋅ g,i=k ⋅ (k1) ⋅ 1 K 1 (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k) f ⋅ g,i=k(rho) (k1) ⋅ 1))

= (mu K (i1) ⋅ f ⋅ g K 1 u)
∈ B((g(f((i1)(rho)));u))

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. composition-uniformity(Gamma.A;B;cB) 7. I : fset(\mBbbN{}) 8. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\} 9. rho : Gamma(I+i) 10. phi : \mBbbF{}(I) 11. mu : I@0:fset(\mBbbN{}) {}\mrightarrow{} a:I+i,s(phi)(I@0) {}\mrightarrow{} (\mPi{}A B)<rho> o iota(a) 12. \mforall{}I@0,J:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I@0. \mforall{}a:I+i,s(phi)(I@0). ((mu I@0 a a f) = (mu J f(a))) 13. lambda : cubical-path-0(Gamma;\mPi{}A B;I;i;rho;phi;mu) 14. J : fset(\mBbbN{}) 15. f : J {}\mrightarrow{} I 16. (phi f) = 1 17. K : fset(\mBbbN{}) 18. g : K {}\mrightarrow{} J 19. u : A(g(f((i1)(rho)))) 20. k : \mBbbN{} 21. \mneg{}k \mmember{} K 22. v : B((k1)((f \mcdot{} g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k)))) 23. \mforall{}J@0:fset(\mBbbN{}). \mforall{}f@0:\{f1:J@0 {}\mrightarrow{} K| (f \mcdot{} g(phi) f1) = 1\} . ((v (k1)((f \mcdot{} g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k))) f@0) = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f \mcdot{} g;k; pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k))((k1) \mcdot{} f@0)) 24. (v (k1)((f \mcdot{} g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k))) 1) = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f \mcdot{} g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k))((k1) \mcdot{} 1) 25. (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k) f \mcdot{} g,i=k(rho) (k1)) = u 26. A((k1)(f \mcdot{} g,i=k(rho))) = A(g(f((i1)(rho)))) 27. (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k) f \mcdot{} g,i=k(rho) (k1) \mcdot{} 1) = u 28. (i1) \mcdot{} f \mmember{} I+i,s(phi)(J) 29. (\mlambda{}K@0,g@0. (mu J (i1) \mcdot{} f K@0 g \mcdot{} g@0)) = (mu K (i1) \mcdot{} f \mcdot{} g) 30. f \mcdot{} g,i=k \mcdot{} (k1) \mcdot{} 1 = (i1) \mcdot{} f \mcdot{} g 31. (mu J (i1) \mcdot{} f K g \mcdot{} 1) = (mu K (i1) \mcdot{} f \mcdot{} g K 1) 32. A(1(<rho> K (i1) \mcdot{} f \mcdot{} g)) = A(g(f((i1)(rho)))) 33. (mu J (i1) \mcdot{} f K g \mcdot{} 1 u) = (mu K (i1) \mcdot{} f \mcdot{} g K 1 u) \mvdash{} (mu J (i1) \mcdot{} f K g u) = (mu K f \mcdot{} g,i=k \mcdot{} (k1) \mcdot{} 1 K 1 (pi-comp-nu(Gamma;A;cA;I;i;rho;K;f \mcdot{} g;u;k) f \mcdot{} g,i=k(rho) (k1) \mcdot{} 1)) By Latex: (NthHypEqGen (-1) THEN EqCD THEN Try (Trivial)) Home Index