---

Step * of Lemma composition-op-uniformity

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[comp:Gamma ⊢ CompOp(A)].
  ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
  ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
    ((comp I i rho phi u a0 (i1)(rho) g)
    = (comp J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
    ∈ A(g((i1)(rho))))
BY
{ (Auto THEN D 3 THEN Unfold `composition-uniformity` 4 THEN BHyp 4 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[comp:Gamma  \mvdash{}  CompOp(A)].
    \mforall{}I,J:fset(\mBbbN{}).  \mforall{}i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  .  \mforall{}j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  .  \mforall{}g:J  {}\mrightarrow{}  I.  \mforall{}rho:Gamma(I+i).  \mforall{}phi:\mBbbF{}(I).
    \mforall{}u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}.  \mforall{}a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
        ((comp  I  i  rho  phi  u  a0  (i1)(rho)  g)
        =  (comp  J  j  g,i=j(rho)  g(phi)  (u)subset-trans(I+i;J+j;g,i=j;s(phi))  (a0  (i0)(rho)  g)))


By

---

Latex:
(Auto  THEN  D  3  THEN  Unfold  `composition-uniformity`  4  THEN  BHyp  4  THEN  Auto)

---

Home Index