---

Step * of Lemma csm+-comp-m

No Annotations
∀[H,K:j⊢]. ∀[tau:K j⟶ H].  (m o tau++ = tau+ o m ∈ K.𝕀.𝕀 ij⟶ H.𝕀)
BY
{ (Auto THEN (BLemma `csm-equal` THENA Auto) THEN RepeatFor 2 ((FunExt THENA Auto))) }

1
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. I : fset(ℕ)
5. x : K.𝕀.𝕀(I)
⊢ (m o tau++ I x) = (tau+ o m I x) ∈ H.𝕀(I)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].    (m  o  tau++  =  tau+  o  m)


By

---

Latex:
(Auto  THEN  (BLemma  `csm-equal`  THENA  Auto)  THEN  RepeatFor  2  ((FunExt  THENA  Auto)))

---

Home Index