---

Step * of Lemma subset-iota-is-id

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}]. ∀[v:{H, phi ⊢ _}].  (v = (v)iota ∈ {H, phi ⊢ _})
BY
{ Intros }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ v = (v)iota ∈ {H, phi ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[v:\{H,  phi  \mvdash{}  \_\}].    (v  =  (v)iota)


By

---

Latex:
Intros

---

Home Index