Nuprl Lemma : ctt-type-type_wf
∀[X:⊢''']. ∀[T:cttType(X)]. (type(T) ∈ X ⊢level(T) )
Proof
Error : references
Latex:
\mforall{}[X:\mvdash{}''']. \mforall{}[T:cttType(X)]. (type(T) \mmember{} X \mvdash{}level(T) )
Date html generated:
2020_05_21-AM-10_31_01
Last ObjectModification:
2020_05_05-PM-05_32_00
Theory : cubical!type!theory
Home
Index