---

Step * of Lemma csm-composition_wf

No Annotations
∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[comp:Gamma ⊢ CompOp(A)].
  ((comp)sigma ∈ Delta ⊢ CompOp((A)sigma))
BY
{ (ProveWfLemma
   THEN D -1
   THEN Assert ⌜λ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)⌝⋅) }

1
.....assertion..... 
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)
⊢ λ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)

2
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[sigma:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[comp:Gamma  \mvdash{}  CompOp(A)].
    ((comp)sigma  \mmember{}  Delta  \mvdash{}  CompOp((A)sigma))


By

---

Latex:
(ProveWfLemma
  THEN  D  -1
  THEN  Assert  \mkleeneopen{}\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)\mkleeneclose{}\mcdot{})

---

Home Index