---

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

.....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+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
12. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
13. J : fset(ℕ)
14. f : J ⟶ I
15. (phi f) = 1
16. K : fset(ℕ)
17. g : K ⟶ J
18. u : A(g(f((i1)(rho))))
19. k : ℕ
20. ¬k ∈ K
21. v : B((k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))))
22. ∀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))))))
23. (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)))))
⊢ (k1)(f ⋅ g,i=k(rho)) = g(f((i1)(rho))) ∈ Gamma(K)
BY
{ (Auto THEN (Assert r0 < ||a - b|| BY EAuto 1) THEN (Assert r0 ≤ dcd BY Auto)) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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+i,s(phi)  \mvdash{}  \_:(\mPi{}A  B)<rho>  o  iota\}
12.  lambda  :  cubical-path-0(Gamma;\mPi{}A  B;I;i;rho;phi;mu)
13.  J  :  fset(\mBbbN{})
14.  f  :  J  {}\mrightarrow{}  I
15.  (phi  f)  =  1
16.  K  :  fset(\mBbbN{})
17.  g  :  K  {}\mrightarrow{}  J
18.  u  :  A(g(f((i1)(rho))))
19.  k  :  \mBbbN{}
20.  \mneg{}k  \mmember{}  K
21.  v  :  B((k1)((f  \mcdot{}  g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f  \mcdot{}  g;u;k))))
22.  \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))
23.  (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)
\mvdash{}  (k1)(f  \mcdot{}  g,i=k(rho))  =  g(f((i1)(rho)))


By

---

Latex:
(Auto  THEN  (Assert  r0  <  ||a  -  b||  BY  EAuto  1)  THEN  (Assert  r0  \mleq{}  dcd  BY  Auto))

---

Home Index