Nuprl Definition : equivTerm
equivTerm(G;A;B) == encode(Equiv(decode(A);decode(B));equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))
Definitions occuring in Statement :
equiv-comp: equiv-comp(H;A;E;cA;cE),
universe-comp-op: compOp(t),
universe-decode: decode(t),
universe-encode: encode(T;cT),
cubical-equiv: Equiv(T;A)
Definitions occuring in definition :
universe-encode: encode(T;cT),
cubical-equiv: Equiv(T;A),
equiv-comp: equiv-comp(H;A;E;cA;cE),
universe-decode: decode(t),
universe-comp-op: compOp(t)
FDL editor aliases :
equivTerm
Latex:
equivTerm(G;A;B) ==
encode(Equiv(decode(A);decode(B));equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))
Date html generated:
2018_05_23-PM-01_58_04
Last ObjectModification:
2017_11_22-AM-11_33_45
Theory : cubical!type!theory
Home
Index