Nuprl Lemma : context-adjoin-subset2
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}]. sub_cubical_set{j:l}(H, phi.𝕀; H.𝕀, (phi)p)
Proof
Error : references
Latex:
\mforall{}[H:j\mvdash{}]. \mforall{}[phi:\{H \mvdash{} \_:\mBbbF{}\}]. sub\_cubical\_set\{j:l\}(H, phi.\mBbbI{}; H.\mBbbI{}, (phi)p)
Date html generated:
2020_05_21-AM-10_30_19
Last ObjectModification:
2020_04_04-PM-05_21_39
Theory : cubical!type!theory
Home
Index