Nuprl Definition : pres-a0
pres-a0(G;f;t0) == app((f)[0(𝕀)]; t0)
Definitions occuring in Statement :
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)
FDL editor aliases :
pres-a0
Latex:
pres-a0(G;f;t0) == app((f)[0(\mBbbI{})]; t0)
Date html generated:
2016_05_19-AM-10_57_18
Last ObjectModification:
2016_04_17-PM-09_38_38
Theory : cubical!type!theory
Home
Index