Step
*
of Lemma
Kan-cubical-type_wf
∀[X:CubicalSet]. ({X ⊢ _(Kan)} ∈ 𝕌')
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[X:CubicalSet]. (\{X \mvdash{} \_(Kan)\} \mmember{} \mBbbU{}')
By
Latex:
ProveWfLemma
Home
Index