---

Step * of Lemma pi-comp-property

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)]. ∀[I:fset(ℕ)].
∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Gamma(I+i)]. ∀[phi:𝔽(I)]. ∀[mu:{I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}].
∀[lambda:cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)]. ∀[J:fset(ℕ)]. ∀[f:I,phi(J)].
  ((pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda (i1)(rho) f) = mu((i1) ⋅ f) ∈ ΠA B(f((i1)(rho))))
BY
{ (Intros
   THEN (RWO "cubical-subset-I_cube" (-1) THENA Auto)
   THEN D -1
   THEN (Assert (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda (i1)(rho) f) ∈ ΠA B(f((i1)(rho))) BY
               Auto)
   THEN RepUR ``cubical-pi cubical-pi-family`` -1
   THEN (MemTypeHD (-1) THENA Auto)
   THEN RepUR ``cubical-pi cubical-pi-family`` 0
   THEN EqTypeCD
   THEN Auto) }

1
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. i : {i:ℕ| ¬i ∈ I} 
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
11. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
12. J : fset(ℕ)
13. f : J ⟶ I
14. (phi f) = 1
15. (λK,g. (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g))
= (λK,g. (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g))
∈ (J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ J ⟶ u:A(f@0(f((i1)(rho)))) ⟶ B((f@0(f((i1)(rho)));u)))
16. ∀J@0,K:fset(ℕ). ∀f@0:J@0 ⟶ J. ∀g:K ⟶ J@0. ∀u:A(f@0(f((i1)(rho)))).
      (((λK,g. (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g)) J@0 f@0 u (f@0(f((i1)(rho)));u) g)
      = ((λK,g. (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g)) K f@0 ⋅ g (u f@0(f((i1)(rho))) g))
      ∈ B(g((f@0(f((i1)(rho)));u))))
⊢ (λK,g. (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g))
= mu((i1) ⋅ f)
∈ (J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ J ⟶ u:A(f@0(f((i1)(rho)))) ⟶ B((f@0(f((i1)(rho)));u)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma.A  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].
\mforall{}[cB:Gamma.A  \mvdash{}  CompOp(B)].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[rho:Gamma(I+i)].  \mforall{}[phi:\mBbbF{}(I)].
\mforall{}[mu:\{I+i,s(phi)  \mvdash{}  \_:(\mPi{}A  B)<rho>  o  iota\}].  \mforall{}[lambda:cubical-path-0(Gamma;\mPi{}A  B;I;i;rho;phi;mu)].
\mforall{}[J:fset(\mBbbN{})].  \mforall{}[f:I,phi(J)].
    ((pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  (i1)(rho)  f)  =  mu((i1)  \mcdot{}  f))


By

---

Latex:
(Intros
  THEN  (RWO  "cubical-subset-I\_cube"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  (i1)(rho)  f)  \mmember{}  \mPi{}A  B(f((i1)(rho)))  BY
                          Auto)
  THEN  RepUR  ``cubical-pi  cubical-pi-family``  -1
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  RepUR  ``cubical-pi  cubical-pi-family``  0
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index