Step
*
of Lemma
subset-cubical-type
No Annotations
∀[X,Y:j⊢].  {X ⊢ _} ⊆r {Y ⊢ _} supposing sub_cubical_set{j:l}(Y; X)
BY
{ PresheafMLTTInstance Obid: subset-presheaf-type⋅ }
Latex:
Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].    \{X  \mvdash{}  \_\}  \msubseteq{}r  \{Y  \mvdash{}  \_\}  supposing  sub\_cubical\_set\{j:l\}(Y;  X)
By
Latex:
PresheafMLTTInstance  Obid:  subset-presheaf-type\mcdot{}
Home
Index