Nuprl Definition : compU
compU() ==
λG,s,phi,E,A. encode(Glue [phi ⟶ (decode((E)[1(𝕀)]);equiv-fun(equivU(G, phi;(decode(E))-;(compOp(E))-)))] decode(A);
cfun-to-cop(G;Glue [phi ⟶ (decode((E)[1(𝕀)]);equiv-fun(equivU(G, phi;(decode(E))-;
(compOp(E))-)))] decode(A)
;comp(Glue [phi ⟶ (decode((E)[1(𝕀)]), equivU(G, phi;(decode(E))-;(compOp(E))-))]
decode(A)) ))
Definitions occuring in Statement :
equivU: equivU(G;E;cE),
universe-comp-op: compOp(t),
universe-decode: decode(t),
universe-encode: encode(T;cT),
glue-comp: comp(Glue [phi ⟶ (T, f)] A) ,
glue-type: Glue [phi ⟶ (T;w)] A,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
comp-op-to-comp-fun: cop-to-cfun(cA),
rev-type-line-comp: (cA)-,
rev-type-line: (A)-,
csm-composition: (comp)sigma,
equiv-fun: equiv-fun(f),
context-subset: Gamma, phi,
interval-1: 1(𝕀),
csm-id-adjoin: [u],
csm-ap-term: (t)s,
lambda: λx.A[x]
Definitions occuring in definition :
universe-comp-op: compOp(t),
rev-type-line-comp: (cA)-,
universe-decode: decode(t),
rev-type-line: (A)-,
context-subset: Gamma, phi,
equivU: equivU(G;E;cE),
interval-1: 1(𝕀),
csm-id-adjoin: [u],
csm-composition: (comp)sigma,
comp-op-to-comp-fun: cop-to-cfun(cA),
csm-ap-term: (t)s,
glue-comp: comp(Glue [phi ⟶ (T, f)] A) ,
equiv-fun: equiv-fun(f),
glue-type: Glue [phi ⟶ (T;w)] A,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
universe-encode: encode(T;cT),
lambda: λx.A[x]
FDL editor aliases :
compU
Latex:
compU() ==
\mlambda{}G,s,phi,E,A. encode(Glue [phi \mvdash{}\mrightarrow{} (decode((E)[1(\mBbbI{})]);equiv-fun(equivU(G, phi;(decode(E))-;
(compOp(E))-)))] decode(A);
cfun-to-cop(G;Glue [phi \mvdash{}\mrightarrow{} (decode((E)[1(\mBbbI{})]);
equiv-fun(equivU(G, phi;(decode(E))-;
(compOp(E))-)))] decode(A)
;comp(Glue [phi \mvdash{}\mrightarrow{} (decode((E)[1(\mBbbI{})]), equivU(G, phi;(decode(E))-;
(compOp(E))-))]
decode(A)) ))
Date html generated:
2017_01_10-PM-00_12_17
Last ObjectModification:
2016_12_25-AM-01_12_02
Theory : cubical!type!theory
Home
Index