---

Step * 2 of Lemma csm-composition_wf


1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
6. composition-uniformity(Gamma;A;comp)
7. λI,i,rho. (comp I i (sigma)rho) ∈ I:fset(ℕ)
   ⟶ i:{i:ℕ| ¬i ∈ I} 
   ⟶ rho:Delta(I+i)
   ⟶ phi:𝔽(I)
   ⟶ u:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
   ⟶ cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
   ⟶ cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u)
⊢ λI,i,rho. (comp I i (sigma)rho) ∈ Delta ⊢ CompOp((A)sigma)
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
6. composition-uniformity(Gamma;A;comp)
7. λI,i,rho. (comp I i (sigma)rho) ∈ I:fset(ℕ)
   ⟶ i:{i:ℕ| ¬i ∈ I} 
   ⟶ rho:Delta(I+i)
   ⟶ phi:𝔽(I)
   ⟶ u:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
   ⟶ cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
   ⟶ cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u)
⊢ composition-uniformity(Delta;(A)sigma;λI,i,rho. (comp I i (sigma)rho))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  sigma  :  Delta  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  comp  :  I:fset(\mBbbN{})
{}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
{}\mrightarrow{}  rho:Gamma(I+i)
{}\mrightarrow{}  phi:\mBbbF{}(I)
{}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
{}\mrightarrow{}  cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{}  cubical-path-1(Gamma;A;I;i;rho;phi;u)
6.  composition-uniformity(Gamma;A;comp)
7.  \mlambda{}I,i,rho.  (comp  I  i  (sigma)rho)  \mmember{}  I:fset(\mBbbN{})
      {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
      {}\mrightarrow{}  rho:Delta(I+i)
      {}\mrightarrow{}  phi:\mBbbF{}(I)
      {}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}
      {}\mrightarrow{}  cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
      {}\mrightarrow{}  cubical-path-1(Delta;(A)sigma;I;i;rho;phi;u)
\mvdash{}  \mlambda{}I,i,rho.  (comp  I  i  (sigma)rho)  \mmember{}  Delta  \mvdash{}  CompOp((A)sigma)


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index