Nuprl Definition : univ-a
univ-a(G;A;B) == cubical-lam(G;EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))
Definitions occuring in Statement :
equiv-path: EquivPath(G;A;B;f),
universe-decode: decode(t),
cubical-equiv: Equiv(T;A),
cubical-lam: cubical-lam(X;b),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
universe-decode: decode(t),
cubical-equiv: Equiv(T;A),
cube-context-adjoin: X.A,
equiv-path: EquivPath(G;A;B;f),
cubical-lam: cubical-lam(X;b)
FDL editor aliases :
univ-a
Latex:
univ-a(G;A;B) == cubical-lam(G;EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))
Date html generated:
2017_01_10-PM-00_22_44
Last ObjectModification:
2017_01_02-AM-00_12_22
Theory : cubical!type!theory
Home
Index