Nuprl Definition : equiv_path
equiv_path(G;A;B;f) ==
let T = equiv-path1(G;decode(A);decode(B);f) in
let C = equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f) in
encode(T;cfun-to-cop(G.𝕀;T;C))
Definitions occuring in Statement :
equiv-path2: equiv-path2(G;A;B;cA;cB;f),
equiv-path1: equiv-path1(G;A;B;f),
universe-comp-fun: CompFun(A),
universe-decode: decode(t),
universe-encode: encode(T;cT),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
interval-type: 𝕀,
cube-context-adjoin: X.A,
let: let
Definitions occuring in definition :
interval-type: 𝕀,
cube-context-adjoin: X.A,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
universe-encode: encode(T;cT),
universe-comp-fun: CompFun(A),
universe-decode: decode(t),
equiv-path2: equiv-path2(G;A;B;cA;cB;f),
let: let,
equiv-path1: equiv-path1(G;A;B;f)
FDL editor aliases :
equiv_path
Latex:
equiv\_path(G;A;B;f) ==
let T = equiv-path1(G;decode(A);decode(B);f) in
let C = equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f) in
encode(T;cfun-to-cop(G.\mBbbI{};T;C))
Date html generated:
2017_01_10-PM-00_21_08
Last ObjectModification:
2017_01_01-PM-10_26_17
Theory : cubical!type!theory
Home
Index