Nuprl Definition : pres-c2
pres-c2(G;phi;f;t;t0;cT) == app((f)[1(𝕀)]; comp cT [phi ⊢→ t] t0)
Definitions occuring in Statement :
comp_term: comp cA [phi ⊢→ u] a0,
interval-1: 1(𝕀),
cubical-app: app(w; u),
csm-id-adjoin: [u],
csm-ap-term: (t)s
Definitions occuring in definition :
comp_term: comp cA [phi ⊢→ u] a0,
interval-1: 1(𝕀),
csm-id-adjoin: [u],
csm-ap-term: (t)s,
cubical-app: app(w; u)
FDL editor aliases :
pres-c2
Latex:
pres-c2(G;phi;f;t;t0;cT) == app((f)[1(\mBbbI{})]; comp cT [phi \mvdash{}\mrightarrow{} t] t0)
Date html generated:
2016_05_20-AM-08_43_06
Last ObjectModification:
2016_05_19-PM-02_26_28
Theory : cubical!type!theory
Home
Index