Nuprl Definition : bij-contr
bij-contr(X; A; f; g; cA; b; c) ==
contr-witness(X;app(g; contr-center(c));map-path(X.A;(g)p;contr-path((c)p;app((f)p; q))) + b)
Definitions occuring in Statement :
comp_path: pth_a_b + pth_b_c,
csm-comp-structure: (cA)tau,
contr-witness: contr-witness(X;c;p),
contr-path: contr-path(c;x),
contr-center: contr-center(c),
map-path: map-path(G;f;pth),
cubical-app: app(w; u),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
contr-witness: contr-witness(X;c;p),
contr-center: contr-center(c),
comp_path: pth_a_b + pth_b_c,
csm-comp-structure: (cA)tau,
map-path: map-path(G;f;pth),
cube-context-adjoin: X.A,
contr-path: contr-path(c;x),
cubical-app: app(w; u),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
bij-contr
Latex:
bij-contr(X; A; f; g; cA; b; c) ==
contr-witness(X;app(g; contr-center(c));map-path(X.A;(g)p;contr-path((c)p;app((f)p; q))) + b)
Date html generated:
2018_05_23-AM-11_13_38
Last ObjectModification:
2017_11_07-PM-02_27_44
Theory : cubical!type!theory
Home
Index