---

Step * of Lemma composition-op-nc-e

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[comp:Gamma ⊢ CompOp(A)].
  ∀I:fset(ℕ). ∀i,j:{j:ℕ| ¬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) = (comp I j e(i;j)(rho) phi (u)subset-trans(I+i;I+j;e(i;j);s(phi)) a0) ∈ A((i1)(rho)))
BY
{ (InstLemma `composition-op-uniformity` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D -1 With ⌜I⌝  THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN (InstHyp [⌜1⌝] (-1)⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast')
   THEN (RWO "nc-e'-1" (-1) THENA Auto)
   THEN (Assert A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type BY
               Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. j : {j:ℕ| ¬j ∈ I} 
7. ∀g: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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
⊢ (comp I i rho phi u a0) = (comp I j e(i;j)(rho) phi (u)subset-trans(I+i;I+j;e(i;j);s(phi)) a0) ∈ A((i1)(rho))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[comp:Gamma  \mvdash{}  CompOp(A)].
    \mforall{}I:fset(\mBbbN{}).  \mforall{}i,j:\{j:\mBbbN{}|  \mneg{}j  \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).
        ((comp  I  i  rho  phi  u  a0)  =  (comp  I  j  e(i;j)(rho)  phi  (u)subset-trans(I+i;I+j;e(i;j);s(phi))  a0))


By

---

Latex:
(InstLemma  `composition-op-uniformity`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}I\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (RWO  "nc-e'-1"  (-1)  THENA  Auto)
  THEN  (Assert  A((i1)(rho))  =  A((j1)(e(i;j)(rho)))  BY
                          Auto))

---

Home Index