---

Step * 1 of Lemma pi-comp-property


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)))
BY
{ (RepeatFor 2 (Thin (-1))
   THEN (RepeatFor 3 ((FunExt THENA Auto)) THEN Reduce 0)
   THEN RenameVar `K' (-3)
   THEN RenameVar `g' (-2)) }

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 : fset(ℕ)
16. g : K ⟶ J
17. u : A(g(f((i1)(rho))))
⊢ (pi-comp(Gamma;A;B;cA;cB) I i rho phi mu lambda K f ⋅ g u) = (mu((i1) ⋅ f) K g u) ∈ B((g(f((i1)(rho)));u))

---

Latex:

---

Latex:

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.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
8.  rho  :  Gamma(I+i)
9.  phi  :  \mBbbF{}(I)
10.  mu  :  \{I+i,s(phi)  \mvdash{}  \_:(\mPi{}A  B)<rho>  o  iota\}
11.  lambda  :  cubical-path-0(Gamma;\mPi{}A  B;I;i;rho;phi;mu)
12.  J  :  fset(\mBbbN{})
13.  f  :  J  {}\mrightarrow{}  I
14.  (phi  f)  =  1
15.  (\mlambda{}K,g.  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  K  f  \mcdot{}  g))
=  (\mlambda{}K,g.  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  K  f  \mcdot{}  g))
16.  \mforall{}J@0,K:fset(\mBbbN{}).  \mforall{}f@0:J@0  {}\mrightarrow{}  J.  \mforall{}g:K  {}\mrightarrow{}  J@0.  \mforall{}u:A(f@0(f((i1)(rho)))).
            (((\mlambda{}K,g.  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  K  f  \mcdot{}  g))  J@0  f@0  u  (f@0(f((i1)(rho))\000C);
                                                                                                                                                                u)  g)
            =  ((\mlambda{}K,g.  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  K  f  \mcdot{}  g))  K  f@0  \mcdot{}  g 
                  (u  f@0(f((i1)(rho)))  g)))
\mvdash{}  (\mlambda{}K,g.  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  K  f  \mcdot{}  g))  =  mu((i1)  \mcdot{}  f)


By

---

Latex:
(RepeatFor  2  (Thin  (-1))
  THEN  (RepeatFor  3  ((FunExt  THENA  Auto))  THEN  Reduce  0)
  THEN  RenameVar  `K'  (-3)
  THEN  RenameVar  `g'  (-2))

---

Home Index