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