---

Step * 1 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 : 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))
BY
{ (RepUR ``pi-comp`` 0
   THEN (GenConclTerm ⌜new-name(K)⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `k' (-1)
   THEN D -1
   THEN RepUR ``let`` 0
   THEN DVar `cB'
   THEN GenConclAtAddr [2]
   THEN Thin (-1)
   THEN D -1
   THEN UnfoldTopAb (-1)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma.A(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(B)<rho> o iota}
⟶ cubical-path-0(Gamma.A;B;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma.A;B;I;i;rho;phi;u)
6. composition-uniformity(Gamma.A;B;cB)
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. f : J ⟶ I
15. (phi f) = 1
16. K : fset(ℕ)
17. g : K ⟶ J
18. u : A(g(f((i1)(rho))))
19. k : ℕ
20. ¬k ∈ K
21. v : B((k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))))
22. ∀J@0:fset(ℕ). ∀f@0:K,f ⋅ g(phi)(J@0).
      ((v (k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))) f@0)
      = pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;f ⋅ g;k;pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))((k1) ⋅ f@0)
      ∈ B(f@0((k1)((f ⋅ g,i=k(rho);pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;u;k))))))
⊢ v = (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.  K  :  fset(\mBbbN{})
16.  g  :  K  {}\mrightarrow{}  J
17.  u  :  A(g(f((i1)(rho))))
\mvdash{}  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  mu  lambda  K  f  \mcdot{}  g  u)  =  (mu((i1)  \mcdot{}  f)  K  g  u)


By

---

Latex:
(RepUR  ``pi-comp``  0
  THEN  (GenConclTerm  \mkleeneopen{}new-name(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `k'  (-1)
  THEN  D  -1
  THEN  RepUR  ``let``  0
  THEN  DVar  `cB'
  THEN  GenConclAtAddr  [2]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  UnfoldTopAb  (-1))

---

Home Index