Nuprl Definition : comp-path
comp-path(G;cA;a;pth_a_b;pth_b_c) ==
<>(comp ((cA)p)p [((q=0) ∨ (q=1)) ⟶ ((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+)] path-eta(pth_a_b))
Definitions occuring in Statement :
comp_term: comp cA [phi ⟶ u] a0,
csm-comp-structure: (cA)tau,
cubical-refl: refl(a),
term-to-path: <>(a),
path-eta: path-eta(pth),
case-term: (u ∨ v),
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
Definitions occuring in definition :
path-eta: path-eta(pth),
cc-fst: p,
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm+: tau+,
csm-ap-term: (t)s,
cubical-refl: refl(a),
cc-snd: q,
face-zero: (i=0),
case-term: (u ∨ v),
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 :
comp-path
Latex:
comp-path(G;cA;a;pth\_a$_{b}$;pth\_b$_{c}$) ==
<>(comp ((cA)p)p [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} ((path-eta(refl(a)))p+ \mvee{} (path-eta(pth\_b$_{c}\000C$))p+)]
path-eta(pth\_a$_{b}$))
Date html generated:
2017_01_10-AM-09_52_45
Last ObjectModification:
2017_01_06-PM-01_30_45
Theory : cubical!type!theory
Home
Index