Step * of Lemma subset-cubical-type

No Annotations
[X,Y:j⊢].  {X ⊢ _} ⊆{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