---

Step * of Lemma csm-m-comp-0

No Annotations
∀[H:j⊢]. ([0(𝕀)] o p = m o [0(𝕀)] ∈ H.𝕀 ij⟶ H.𝕀)
BY
{ Intros }

1
1. H : CubicalSet{j}
⊢ [0(𝕀)] o p = m o [0(𝕀)] ∈ H.𝕀 ij⟶ H.𝕀

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  ([0(\mBbbI{})]  o  p  =  m  o  [0(\mBbbI{})])


By

---

Latex:
Intros

---

Home Index