Nuprl Definition : uabeta_aux
uabeta_aux(G;A;B;f) ==
let b = app(equiv-fun((f)p); q) in
let b' = transprt-const(G.decode(A);(CompFun(B))p;b) in
let pth1 = trans-const-path(G.decode(A);(CompFun(B))p;b') in
let pth2 = trans-const-path(G.decode(A);(CompFun(B))p;b) in
pth1 + pth2
Definitions occuring in Statement :
universe-comp-fun: CompFun(A),
universe-decode: decode(t),
comp_path: pth_a_b + pth_b_c,
trans-const-path: trans-const-path(G;cA;a),
transprt-const: transprt-const(G;cA;a),
csm-comp-structure: (cA)tau,
equiv-fun: equiv-fun(f),
cubical-app: app(w; u),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
let: let
Definitions occuring in definition :
cubical-app: app(w; u),
equiv-fun: equiv-fun(f),
csm-ap-term: (t)s,
cc-snd: q,
transprt-const: transprt-const(G;cA;a),
let: let,
trans-const-path: trans-const-path(G;cA;a),
comp_path: pth_a_b + pth_b_c,
csm-comp-structure: (cA)tau,
cube-context-adjoin: X.A,
universe-decode: decode(t),
cc-fst: p,
universe-comp-fun: CompFun(A)
FDL editor aliases :
uabeta_aux
Latex:
uabeta\_aux(G;A;B;f) ==
let b = app(equiv-fun((f)p); q) in
let b' = transprt-const(G.decode(A);(CompFun(B))p;b) in
let pth1 = trans-const-path(G.decode(A);(CompFun(B))p;b') in
let pth2 = trans-const-path(G.decode(A);(CompFun(B))p;b) in
pth1 + pth2
Date html generated:
2018_05_23-PM-06_21_41
Last ObjectModification:
2017_10_31-AM-10_56_20
Theory : cubical!type!theory
Home
Index