Nuprl Definition : path_comp
path_comp(G;A;a;b;cA) ==
λH,sigma,phi,u,a0. <>(comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q)] (a0)p @ q)
Definitions occuring in Statement :
path_term: path_term(phi; w; a; b; r),
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
term-to-path: <>(a),
cubical-path-app: pth @ r,
face-zero: (i=0),
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,
lambda: λx.A[x]
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
cubical-path-app: pth @ r,
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm+: tau+,
path_term: path_term(phi; w; a; b; r),
face-one: (i=1),
face-zero: (i=0),
face-or: (a ∨ b),
csm-comp-structure: (cA)tau,
comp_term: comp cA [phi ⊢→ u] a0,
term-to-path: <>(a),
lambda: λx.A[x]
FDL editor aliases :
path_comp
Latex:
path\_comp(G;A;a;b;cA) ==
\mlambda{}H,sigma,phi,u,a0. <>(comp ((cA)sigma)p+ [((phi)p \mvee{} ((q=0) \mvee{} (q=1))) \mvdash{}\mrightarrow{} path\_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q)] (a0)p @ q)
Date html generated:
2016_06_16-PM-02_19_10
Last ObjectModification:
2016_06_09-PM-06_31_31
Theory : cubical!type!theory
Home
Index