Nuprl Definition : comp-U
comp-U() ==
λG,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 :
lambda: λx.A[x],
universe-encode: encode(T;cT),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
glue-type: Glue [phi ⊢→ (T;w)] A,
equiv-fun: equiv-fun(f),
glue-comp: comp(Glue [phi ⊢→ (T, f)] A) ,
csm-ap-term: (t)s,
comp-op-to-comp-fun: cop-to-cfun(cA),
csm-composition: (comp)sigma,
csm-id-adjoin: [u],
interval-1: 1(𝕀),
equivU: equivU(G;E;cE),
context-subset: Gamma, phi,
rev-type-line: (A)-,
universe-decode: decode(t),
rev-type-line-comp: (cA)-,
universe-comp-op: compOp(t)
FDL editor aliases :
comp-U
Latex:
comp-U() ==
\mlambda{}G,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:
2020_05_20-PM-07_21_23
Last ObjectModification:
2020_03_20-PM-07_50_43
Theory : cubical!type!theory
Home
Index