Nuprl Definition : ctt-is-fibrant
ctt-is-fibrant(t) == (¬bisvarterm(t)) ∧b ctt-op-sort(term-opr(t)) =a "fibrant"
Definitions occuring in Statement :
ctt-op-sort: ctt-op-sort(f),
term-opr: term-opr(t),
isvarterm: isvarterm(t),
band: p ∧b q,
bnot: ¬bb,
eq_atom: x =a y,
token: "$token"
Definitions occuring in definition :
band: p ∧b q,
bnot: ¬bb,
isvarterm: isvarterm(t),
eq_atom: x =a y,
ctt-op-sort: ctt-op-sort(f),
term-opr: term-opr(t),
token: "$token"
FDL editor aliases :
ctt-is-fibrant
Latex:
ctt-is-fibrant(t) == (\mneg{}\msubb{}isvarterm(t)) \mwedge{}\msubb{} ctt-op-sort(term-opr(t)) =a "fibrant"
Date html generated:
2020_05_21-AM-10_35_41
Last ObjectModification:
2020_02_12-PM-04_07_26
Theory : cubical!type!theory
Home
Index