---

Step * 1 of Lemma pi-comp-lambda_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. phi : 𝔽(I)
8. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
9. lambda : ΠA B((i0)(rho))
10. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
11. J : fset(ℕ)
12. f : J ⟶ I
13. j : {j:ℕ| ¬j ∈ J} 
14. nu : A(r_j(f,i=1-j(rho)))
⊢ pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu)
  ∈ cubical-path-0(Gamma.A;B;J;j;(f,i=j(rho);nu);f(phi);pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu))
BY
{ (OnVar `lambda' (\h. RepUR ``cubical-pi cubical-pi-family`` h THEN D h)
   THEN Assert ⌜lambda J f (nu r_j(f,i=1-j(rho)) (j0)) ∈ B((j0)((f,i=j(rho);nu)))⌝⋅
   ) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. phi : 𝔽(I)
8. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
9. lambda : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
10. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
      ((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
11. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
12. J : fset(ℕ)
13. f : J ⟶ I
14. j : {j:ℕ| ¬j ∈ J} 
15. nu : A(r_j(f,i=1-j(rho)))
⊢ lambda J f (nu r_j(f,i=1-j(rho)) (j0)) ∈ B((j0)((f,i=j(rho);nu)))

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. phi : 𝔽(I)
8. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
9. lambda : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A(f((i0)(rho))) ⟶ B((f((i0)(rho));u))
10. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f((i0)(rho))).
      ((lambda J f u (f((i0)(rho));u) g) = (lambda K f ⋅ g (u f((i0)(rho)) g)) ∈ B(g((f((i0)(rho));u))))
11. cubical-path-condition(Gamma;ΠA B;I;i;rho;phi;mu;lambda)
12. J : fset(ℕ)
13. f : J ⟶ I
14. j : {j:ℕ| ¬j ∈ J} 
15. nu : A(r_j(f,i=1-j(rho)))
16. lambda J f (nu r_j(f,i=1-j(rho)) (j0)) ∈ B((j0)((f,i=j(rho);nu)))
⊢ pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu)
  ∈ cubical-path-0(Gamma.A;B;J;j;(f,i=j(rho);nu);f(phi);pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  B  :  \{Gamma.A  \mvdash{}  \_\}
4.  I  :  fset(\mBbbN{})
5.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
6.  rho  :  Gamma(I+i)
7.  phi  :  \mBbbF{}(I)
8.  mu  :  \{I+i,s(phi)  \mvdash{}  \_:(\mPi{}A  B)<rho>  o  iota\}
9.  lambda  :  \mPi{}A  B((i0)(rho))
10.  cubical-path-condition(Gamma;\mPi{}A  B;I;i;rho;phi;mu;lambda)
11.  J  :  fset(\mBbbN{})
12.  f  :  J  {}\mrightarrow{}  I
13.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\} 
14.  nu  :  A(r\_j(f,i=1-j(rho)))
\mvdash{}  pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu)
    \mmember{}  cubical-path-0(Gamma.A;B;J;j;(f,i=j(rho);nu);f(phi);pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;
                                                                                                                                        nu))


By

---

Latex:
(OnVar  `lambda'  (\mbackslash{}h.  RepUR  ``cubical-pi  cubical-pi-family``  h  THEN  D  h)
  THEN  Assert  \mkleeneopen{}lambda  J  f  (nu  r\_j(f,i=1-j(rho))  (j0))  \mmember{}  B((j0)((f,i=j(rho);nu)))\mkleeneclose{}\mcdot{}
  )

---

Home Index