---

Step * of Lemma pi-comp_wf3

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)].
  (pi-comp(Gamma;A;B;cA;cB) ∈ 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)
   ⟶ ΠA B((i1)(rho)))
BY
{ (InstLemma `pi-comp_wf2` []
   THEN RepeatFor 5 (ParallelLast')
   THEN RepeatFor 6 ((FunExt THENA Auto))
   THEN RepUR ``cubical-pi cubical-pi-family`` 0
   THEN MemTypeCD
   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. pi-comp(Gamma;A;B;cA;cB) ∈ 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:J ⟶ I
   ⟶ u1:A(f((i1)(rho)))
   ⟶ B((f((i1)(rho));u1))
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. K : fset(ℕ)
15. f : J ⟶ I
16. g : K ⟶ J
17. u : A(f((i1)(rho)))
⊢ (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda J f u (f((i1)(rho));u) g)
= (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g (u f((i1)(rho)) g))
∈ B(g((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)].
    (pi-comp(Gamma;A;B;cA;cB)  \mmember{}  I:fset(\mBbbN{})
      {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
      {}\mrightarrow{}  rho:Gamma(I+i)
      {}\mrightarrow{}  phi:\mBbbF{}(I)
      {}\mrightarrow{}  mu:\{I+i,s(phi)  \mvdash{}  \_:(\mPi{}A  B)<rho>  o  iota\}
      {}\mrightarrow{}  lambda:cubical-path-0(Gamma;\mPi{}A  B;I;i;rho;phi;mu)
      {}\mrightarrow{}  \mPi{}A  B((i1)(rho)))


By

---

Latex:
(InstLemma  `pi-comp\_wf2`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  RepeatFor  6  ((FunExt  THENA  Auto))
  THEN  RepUR  ``cubical-pi  cubical-pi-family``  0
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index