Nuprl Definition : transEquivbeta-type
transEquivbeta-type{i:l}(G;A;B) ==
ΠEquiv(decode(A);decode(B)) Π(decode(A))p (Path_((decode(B))p)p app(transEquivFun(app(UA; (q)p)); q)
app(equiv-fun((q)p); q))
Definitions occuring in Statement :
transEquiv-trans: transEquivFun(p),
univ-a: UA,
universe-decode: decode(t),
equiv-fun: equiv-fun(f),
cubical-equiv: Equiv(T;A),
path-type: (Path_A a b),
cubical-app: app(w; u),
cubical-pi: ΠA B,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s
Definitions occuring in definition :
cubical-pi: ΠA B,
path-type: (Path_A a b),
transEquiv-trans: transEquivFun(p),
univ-a: UA,
cube-context-adjoin: X.A,
cubical-equiv: Equiv(T;A),
csm-ap-type: (AF)s,
universe-decode: decode(t),
cubical-app: app(w; u),
equiv-fun: equiv-fun(f),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
transEquivbeta-type
Latex:
transEquivbeta-type\{i:l\}(G;A;B) ==
\mPi{}Equiv(decode(A);decode(B)) \mPi{}(decode(A))p (Path\_((decode(B))p)p app(transEquivFun(app(UA; (q)p));
q) app(equiv-fun((q)p); q))
Date html generated:
2018_05_23-PM-06_26_00
Last ObjectModification:
2017_11_24-AM-10_38_20
Theory : cubical!type!theory
Home
Index