Nuprl Definition : ctt-meaning-type
ctt-meaning-type{i:l}(X;t) ==
if isvarterm(t) then cttTerm(X)
if ctt-op-sort(term-opr(t)) =a "fibrant" then cttType(X)
if ctt-op-sort(term-opr(t)) =a "type" then lvl:ℕ4 × {X ⊢lvl _}
else cttTerm(X)
fi
Definitions occuring in Statement :
ctt-op-sort: ctt-op-sort(f),
ctt-type-meaning: cttType(X),
ctt-term-meaning: cttTerm(X),
ctt-level-type: {X ⊢lvl _},
term-opr: term-opr(t),
isvarterm: isvarterm(t),
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
product: x:A × B[x],
natural_number: $n,
token: "$token"
Definitions occuring in definition :
isvarterm: isvarterm(t),
ctt-type-meaning: cttType(X),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
ctt-op-sort: ctt-op-sort(f),
term-opr: term-opr(t),
token: "$token",
product: x:A × B[x],
int_seg: {i..j-},
natural_number: $n,
ctt-level-type: {X ⊢lvl _},
ctt-term-meaning: cttTerm(X)
FDL editor aliases :
ctt-meaning-type
Latex:
ctt-meaning-type\{i:l\}(X;t) ==
if isvarterm(t) then cttTerm(X)
if ctt-op-sort(term-opr(t)) =a "fibrant" then cttType(X)
if ctt-op-sort(term-opr(t)) =a "type" then lvl:\mBbbN{}4 \mtimes{} \{X \mvdash{}lvl \_\}
else cttTerm(X)
fi
Date html generated:
2020_05_21-AM-10_32_38
Last ObjectModification:
2020_05_05-AM-10_15_11
Theory : cubical!type!theory
Home
Index