Nuprl Definition : uabeta
uabeta(G;A;B) == (λ(λuabeta_aux(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))
Definitions occuring in Statement :
uabeta_aux: uabeta_aux(G;A;B;f),
universe-decode: decode(t),
cubical-equiv: Equiv(T;A),
cubical-lambda: (λb),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
cubical-lambda: (λb),
uabeta_aux: uabeta_aux(G;A;B;f),
cube-context-adjoin: X.A,
cubical-equiv: Equiv(T;A),
universe-decode: decode(t),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
uabeta
Latex:
uabeta(G;A;B) == (\mlambda{}(\mlambda{}uabeta\_aux(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))
Date html generated:
2018_05_23-PM-06_23_54
Last ObjectModification:
2017_11_01-AM-10_37_09
Theory : cubical!type!theory
Home
Index