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