Nuprl Definition : rev_fill_term
rev_fill_term(Gamma;cA;phi;u;a1) == (fill rev-type-comp(Gamma;cA) [phi ⟶ (u)(p;1-(q))] a1)(p;1-(q))
Definitions occuring in Statement :
fill_term: fill cA [phi ⟶ u] a0,
rev-type-comp: rev-type-comp(Gamma;cA),
interval-rev: 1-(r),
csm-adjoin: (s;u),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
cc-snd: q,
interval-rev: 1-(r),
cc-fst: p,
csm-adjoin: (s;u),
csm-ap-term: (t)s,
rev-type-comp: rev-type-comp(Gamma;cA),
fill_term: fill cA [phi ⟶ u] a0
FDL editor aliases :
rev_fill_term
Latex:
rev\_fill\_term(Gamma;cA;phi;u;a1) ==
(fill rev-type-comp(Gamma;cA) [phi \mvdash{}\mrightarrow{} (u)(p;1-(q))] a1)(p;1-(q))
Date html generated:
2016_10_28-AM-08_04_26
Last ObjectModification:
2016_07_20-PM-02_20_04
Theory : cubical!type!theory
Home
Index