Nuprl Lemma : ctt-type-meaning_wf
∀[X:⊢''']. (cttType(X) ∈ 𝕌{i'''''})
Proof
Error : references
Latex:
\mforall{}[X:\mvdash{}''']. (cttType(X) \mmember{} \mBbbU{}\{i'''''\})
Date html generated:
2020_05_21-AM-10_30_45
Last ObjectModification:
2020_05_03-PM-05_24_12
Theory : cubical!type!theory
Home
Index