---

Step * of Lemma equal-composition-op2

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[c1,c2:Gamma ⊢ CompOp(A)].
  c1 = c2 ∈ Gamma ⊢ CompOp(A) 
  supposing ∀I:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ 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).
              ((c1 I i rho phi u a0) = (c2 I i rho phi u a0) ∈ A((i1)(rho)))
BY
{ (InstLemma `equal-composition-op` []
   THEN RepeatFor 5 (ParallelLast')
   THEN RepeatFor 6 ((FunExt THENA Auto))
   THEN (Assert c1 I i rho phi u x ∈ cubical-path-1(Gamma;A;I;i;rho;phi;u) BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN EqTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[c1,c2:Gamma  \mvdash{}  CompOp(A)].
    c1  =  c2 
    supposing  \mforall{}I:fset(\mBbbN{}).  \mforall{}i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  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).
                            ((c1  I  i  rho  phi  u  a0)  =  (c2  I  i  rho  phi  u  a0))


By

---

Latex:
(InstLemma  `equal-composition-op`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  RepeatFor  6  ((FunExt  THENA  Auto))
  THEN  (Assert  c1  I  i  rho  phi  u  x  \mmember{}  cubical-path-1(Gamma;A;I;i;rho;phi;u)  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index