---

Step * of Lemma 0-comp-cc-fst-comp-m

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

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

---

Latex:

---

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


By

---

Latex:
Intros

---

Home Index