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