---

Step * of Lemma csm-composition-comp

No Annotations
∀[X,Y,Z:j⊢]. ∀[s1:Z j⟶ Y]. ∀[s2:Y j⟶ X]. ∀[A:{X ⊢ _}]. ∀[comp:X ⊢ CompOp(A)].
  (((comp)s2)s1 = (comp)s2 o s1 ∈ Z ⊢ CompOp((A)s2 o s1))
BY
{ ((Intros THEN (BLemma `equal-composition-op` THENA Auto))
   THEN RepeatFor 6 ((FunExt THENA Auto))
   THEN RepUR ``csm-composition`` 0
   THEN DVar `comp') }

1
1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. Z : CubicalSet{j}
4. s1 : Z j⟶ Y
5. s2 : Y j⟶ X
6. A : {X ⊢ _}
7. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:X(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(X;A;I;i;rho;phi;u)
⟶ cubical-path-1(X;A;I;i;rho;phi;u)
8. composition-uniformity(X;A;comp)
9. I : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. rho : Z(I+i)
12. phi : 𝔽(I)
13. u : {I+i,s(phi) ⊢ _:((A)s2 o s1)<rho> o iota}
14. x : cubical-path-0(Z;(A)s2 o s1;I;i;rho;phi;u)
⊢ (comp I i (s2)(s1)rho phi u x) = (comp I i (s2 o s1)rho phi u x) ∈ cubical-path-1(Z;(A)s2 o s1;I;i;rho;phi;u)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y,Z:j\mvdash{}].  \mforall{}[s1:Z  j{}\mrightarrow{}  Y].  \mforall{}[s2:Y  j{}\mrightarrow{}  X].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[comp:X  \mvdash{}  CompOp(A)].
    (((comp)s2)s1  =  (comp)s2  o  s1)


By

---

Latex:
((Intros  THEN  (BLemma  `equal-composition-op`  THENA  Auto))
  THEN  RepeatFor  6  ((FunExt  THENA  Auto))
  THEN  RepUR  ``csm-composition``  0
  THEN  DVar  `comp')

---

Home Index