---

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

.....assertion..... 
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
⊢ pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k) = pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k) ∈ A(g ⋅ f,i=k(rho))
BY
{ (RepUR ``pi-comp-nu`` 0
   THEN (GenConclTerm ⌜fill_from_comp(Gamma;A;cA)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `fill' (-1)
   THEN D -1
   THEN RepUR ``let`` 0
   THEN InferEqualType
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
6: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
⊢ (fill K k g ⋅ f,i=1-k(rho) 0 () u) = (fill K k f,j=1-k(g,i=j(rho)) 0 () u) ∈ A(g ⋅ f,i=1-k(rho))

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  pi-comp-nu(Gamma;A;cA;I;i;rho;K;g  \mcdot{}  f;u;k)  =  pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k)


By

---

Latex:
(RepUR  ``pi-comp-nu``  0
  THEN  (GenConclTerm  \mkleeneopen{}fill\_from\_comp(Gamma;A;cA)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `fill'  (-1)
  THEN  D  -1
  THEN  RepUR  ``let``  0
  THEN  InferEqualType
  THEN  EqCD
  THEN  Auto)

---

Home Index