Nuprl Definition : ctt-term-type-is
type(t)=T == type(t) = T ∈ {X ⊢''' _}
Definitions occuring in Statement :
ctt-term-type: type(t),
cubical-type: {X ⊢ _},
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
cubical-type: {X ⊢ _},
ctt-term-type: type(t)
FDL editor aliases :
ctty-is
ctty-is
Latex:
type(t)=T == type(t) = T
Date html generated:
2020_05_20-PM-07_51_47
Last ObjectModification:
2020_05_05-PM-01_59_32
Theory : cubical!type!theory
Home
Index