Step
*
of Lemma
cubical-snd-pair
No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}]. (cubical-pair(u;v).2 = v ∈ {X ⊢ _:(B)[u]})
BY
{ PresheafMLTTInstance Obid: presheaf-snd-pair⋅ }
Latex:
Latex:
No Annotations
\mforall{}[X:j\mvdash{}]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[B:\{X.A \mvdash{} \_\}]. \mforall{}[u:\{X \mvdash{} \_:A\}]. \mforall{}[v:\{X \mvdash{} \_:(B)[u]\}].
(cubical-pair(u;v).2 = v)
By
Latex:
PresheafMLTTInstance Obid: presheaf-snd-pair\mcdot{}
Home
Index