---

Step * 1 1 2 1 1 2 1 2 5 1 of Lemma pi-comp-uniformity

.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. I : fset(ℕ)
7. J : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I} 
9. j : {j:ℕ| ¬j ∈ J} 
10. g : J ⟶ I
11. rho : Gamma(I+i)
12. phi : 𝔽(I)
13. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
14. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
15. K : fset(ℕ)
16. f : K ⟶ J
17. u : A(f(g((i1)(rho))))
18. k : {i:ℕ| ¬i ∈ K} 
19. g ⋅ f,i=1-k = g,i=j ⋅ f,j=1-k ∈ K+k ⟶ I+i
20. 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)))} 
21. filling-uniformity(Gamma;A;fill)
22. A(r_k(g ⋅ f,i=1-k(rho))) = A(g ⋅ f,i=k(rho)) ∈ Type
23. f,j=1-k(g,i=j(rho)) = g ⋅ f,i=1-k(rho) ∈ Gamma(K+k)
24. f,j=1-k(g,i=j(rho))
= g ⋅ f,i=1-k(rho)
∈ {z:Gamma(K+k)| (z = f,j=1-k(g,i=j(rho)) ∈ Gamma(K+k)) ∧ (z = g ⋅ f,i=1-k(rho) ∈ Gamma(K+k))} 
25. z : Gamma(K+k)
26. (z = f,j=1-k(g,i=j(rho)) ∈ Gamma(K+k)) ∧ (z = g ⋅ f,i=1-k(rho) ∈ Gamma(K+k))
27. (fill K k z 0 () u)
= (fill K k z 0 () u)
∈ {a:A(z)| (section-iota(Gamma;A;K+k;z;a) = () ∈ {K+k,s(0) ⊢ _:(A)<z> o iota}) ∧ ((a z (k0)) = u ∈ A((k0)(z)))} 
28. x : {a:A(z)| (section-iota(Gamma;A;K+k;z;a) = () ∈ {K+k,s(0) ⊢ _:(A)<z> o iota}) ∧ ((a z (k0)) = u ∈ A((k0)(z)))} 
⊢ x ∈ A(g ⋅ f,i=1-k(rho))
BY
{ (D -1 THEN InferEqualType THEN 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  :  Gamma.A  \mvdash{}  CompOp(B)
6.  I  :  fset(\mBbbN{})
7.  J  :  fset(\mBbbN{})
8.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
9.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\} 
10.  g  :  J  {}\mrightarrow{}  I
11.  rho  :  Gamma(I+i)
12.  phi  :  \mBbbF{}(I)
13.  mu  :  \{I+i,s(phi)  \mvdash{}  \_:(\mPi{}A  B)<rho>  o  iota\}
14.  lambda  :  cubical-path-0(Gamma;\mPi{}A  B;I;i;rho;phi;mu)
15.  K  :  fset(\mBbbN{})
16.  f  :  K  {}\mrightarrow{}  J
17.  u  :  A(f(g((i1)(rho))))
18.  k  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  K\} 
19.  g  \mcdot{}  f,i=1-k  =  g,i=j  \mcdot{}  f,j=1-k
20.  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)\} 
21.  filling-uniformity(Gamma;A;fill)
22.  A(r\_k(g  \mcdot{}  f,i=1-k(rho)))  =  A(g  \mcdot{}  f,i=k(rho))
23.  f,j=1-k(g,i=j(rho))  =  g  \mcdot{}  f,i=1-k(rho)
24.  f,j=1-k(g,i=j(rho))  =  g  \mcdot{}  f,i=1-k(rho)
25.  z  :  Gamma(K+k)
26.  (z  =  f,j=1-k(g,i=j(rho)))  \mwedge{}  (z  =  g  \mcdot{}  f,i=1-k(rho))
27.  (fill  K  k  z  0  ()  u)  =  (fill  K  k  z  0  ()  u)
28.  x  :  \{a:A(z)|  (section-iota(Gamma;A;K+k;z;a)  =  ())  \mwedge{}  ((a  z  (k0))  =  u)\} 
\mvdash{}  x  \mmember{}  A(g  \mcdot{}  f,i=1-k(rho))


By

---

Latex:
(D  -1  THEN  InferEqualType  THEN  Auto)

---

Home Index