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