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