Nuprl Definition : transEquiv
transEquiv{i:l}(G;A;p) == cubical-subst(G;cubical-lam(G;equivTerm(G.c𝕌;(A)p;q));p;IdEquiv(G;decode(A)))
Definitions occuring in Statement :
equivTerm: equivTerm(G;A;B),
cubical-subst: cubical-subst(G;f;pth;x),
universe-decode: decode(t),
cubical-universe: c𝕌,
cubical-id-equiv: IdEquiv(X;T),
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 :
cubical-subst: cubical-subst(G;f;pth;x),
cubical-lam: cubical-lam(X;b),
equivTerm: equivTerm(G;A;B),
cube-context-adjoin: X.A,
cubical-universe: c𝕌,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q,
cubical-id-equiv: IdEquiv(X;T),
universe-decode: decode(t)
FDL editor aliases :
transEquiv
Latex:
transEquiv\{i:l\}(G;A;p) ==
cubical-subst(G;cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));p;IdEquiv(G;decode(A)))
Date html generated:
2018_05_23-PM-01_59_11
Last ObjectModification:
2017_11_22-AM-11_42_16
Theory : cubical!type!theory
Home
Index