---

Step * of Lemma id-fiber-center_wf

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}].  (id-fiber-center(X;T) ∈ {X.T ⊢ _:Σ (T)p (Path_((T)p)p (q)p q)})
BY
{ ProveWfLemma }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
⊢ refl(q) ∈ {X.T ⊢ _:((Path_((T)p)p (q)p q))[q]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].    (id-fiber-center(X;T)  \mmember{}  \{X.T  \mvdash{}  \_:\mSigma{}  (T)p  (Path\_((T)p)p  (q)p  q)\})


By

---

Latex:
ProveWfLemma

---

Home Index