Nuprl Definition : uabeta-type
uabeta-type(G;A;B) ==
ΠEquiv(decode(A);decode(B)) Π(decode(A))p (Path_((decode(B))p)p app(PathTransport(app(UA; (q)p)); q)
app(equiv-fun((q)p); q))
Definitions occuring in Statement :
path-trans: PathTransport(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),
path-trans: PathTransport(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 :
uabeta-type
Latex:
uabeta-type(G;A;B) ==
\mPi{}Equiv(decode(A);decode(B)) \mPi{}(decode(A))p (Path\_((decode(B))p)p app(PathTransport(app(UA; (q)p));
q) app(equiv-fun((q)p); q))
Date html generated:
2018_05_23-PM-06_23_23
Last ObjectModification:
2017_10_31-PM-06_39_09
Theory : cubical!type!theory
Home
Index