Nuprl Definition : equiv-term
equiv f [phi ⊢→ (t, c)] a ==
let e = equiv-contr(f;a) in
let u = (contr-path(e;fiber-point(t;c)))p @ q in
comp (cF)p [phi ⊢→ u] contr-center(e)
Definitions occuring in Statement :
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
equiv-contr: equiv-contr(f;a),
fiber-point: fiber-point(t;c),
contr-path: contr-path(c;x),
contr-center: contr-center(c),
cubical-path-app: pth @ r,
interval-type: 𝕀,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
let: let
Definitions occuring in definition :
equiv-contr: equiv-contr(f;a),
let: let,
cubical-path-app: pth @ r,
csm-ap-term: (t)s,
contr-path: contr-path(c;x),
fiber-point: fiber-point(t;c),
cc-snd: q,
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
cube-context-adjoin: X.A,
interval-type: 𝕀,
cc-fst: p,
contr-center: contr-center(c)
FDL editor aliases :
equiv-term
Latex:
equiv f [phi \mvdash{}\mrightarrow{} (t, c)] a ==
let e = equiv-contr(f;a) in
let u = (contr-path(e;fiber-point(t;c)))p @ q in
comp (cF)p [phi \mvdash{}\mrightarrow{} u] contr-center(e)
Date html generated:
2016_06_16-PM-02_32_43
Last ObjectModification:
2016_06_06-PM-04_53_06
Theory : cubical!type!theory
Home
Index