Nuprl Definition : pathtype-comp
pathtype-comp(G;A;cA) == λH,sigma,phi,u,a0. <>comp ((cA)sigma)p+ [(phi)p ⊢→ (u)p+ @ (q)p] (a0)p @ q
Definitions occuring in Statement :
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
term-to-pathtype: <>a,
cubicalpath-app: pth @ r,
interval-type: 𝕀,
csm+: tau+,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
term-to-pathtype: <>a,
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
csm+: tau+,
cube-context-adjoin: X.A,
interval-type: 𝕀,
cubicalpath-app: pth @ r,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
pathtype-comp
Latex:
pathtype-comp(G;A;cA) == \mlambda{}H,sigma,phi,u,a0. <>comp ((cA)sigma)p+ [(phi)p \mvdash{}\mrightarrow{} (u)p+ @ (q)p] (a0)p @ q
Date html generated:
2016_06_16-PM-02_15_28
Last ObjectModification:
2016_06_06-PM-01_36_54
Theory : cubical!type!theory
Home
Index