Nuprl Definition : trans-equiv-path
trans-equiv-path(G;A;B;f) ==
let tr = λb.transprt-const(G.decode(A);(CompFun(B))p;b) in
let b = app(equiv-fun((f)p); q) in
cubical-lam(G;tr (tr b))
Definitions occuring in Statement :
universe-comp-fun: CompFun(A),
universe-decode: decode(t),
transprt-const: transprt-const(G;cA;a),
csm-comp-structure: (cA)tau,
equiv-fun: equiv-fun(f),
cubical-app: app(w; u),
cubical-lam: cubical-lam(X;b),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
let: let,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
transprt-const: transprt-const(G;cA;a),
csm-comp-structure: (cA)tau,
cube-context-adjoin: X.A,
universe-decode: decode(t),
universe-comp-fun: CompFun(A),
let: let,
cubical-app: app(w; u),
equiv-fun: equiv-fun(f),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q,
cubical-lam: cubical-lam(X;b),
apply: f a
FDL editor aliases :
trans-equiv-path
Latex:
trans-equiv-path(G;A;B;f) ==
let tr = \mlambda{}b.transprt-const(G.decode(A);(CompFun(B))p;b) in
let b = app(equiv-fun((f)p); q) in
cubical-lam(G;tr (tr b))
Date html generated:
2018_05_23-PM-06_18_44
Last ObjectModification:
2017_10_30-PM-06_50_29
Theory : cubical!type!theory
Home
Index