Nuprl Lemma : contextof_wf
∀[X:?CubicalContext]. contextof(X) ∈ CubicalContext supposing context-ok(X)
Proof
Error : references
Latex:
\mforall{}[X:?CubicalContext]. contextof(X) \mmember{} CubicalContext supposing context-ok(X)
Date html generated:
2020_05_21-AM-10_31_48
Last ObjectModification:
2020_05_18-PM-09_51_31
Theory : cubical!type!theory
Home
Index