Nuprl Definition : pres
pres f [phi ⊢→ t] t0 == <>(comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p)
Definitions occuring in Statement :
presw: presw(G;phi;f;t;t0;cT),
pres-a0: pres-a0(G;f;t0),
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
term-to-path: <>(a),
face-one: (i=1),
face-or: (a ∨ b),
interval-type: 𝕀,
csm+: tau+,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
pres-a0: pres-a0(G;f;t0),
cc-fst: p,
csm-ap-term: (t)s,
presw: presw(G;phi;f;t;t0;cT),
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm+: tau+,
cc-snd: q,
face-one: (i=1),
face-or: (a ∨ b),
csm-comp-structure: (cA)tau,
comp_term: comp cA [phi ⊢→ u] a0,
term-to-path: <>(a)
FDL editor aliases :
pres
Latex:
pres f [phi \mvdash{}\mrightarrow{} t] t0 ==
<>(comp (cA)p+ [((phi)p \mvee{} (q=1)) \mvdash{}\mrightarrow{} (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p)
Date html generated:
2016_05_19-AM-11_00_31
Last ObjectModification:
2016_04_18-PM-04_43_22
Theory : cubical!type!theory
Home
Index