Nuprl Definition : name-morph
name-morph(I;J) ==
{f:nameset(I) ⟶ extd-nameset(J)|
∀i,j:nameset(I). ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))}
Definitions occuring in Statement :
isname: isname(z),
extd-nameset: extd-nameset(L),
nameset: nameset(L),
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
assert: ↑b,
isname: isname(z),
implies: P ⇒ Q,
extd-nameset: extd-nameset(L),
apply: f a,
equal: s = t ∈ T,
nameset: nameset(L)
FDL editor aliases :
name-morph
Latex:
name-morph(I;J) ==
\{f:nameset(I) {}\mrightarrow{} extd-nameset(J)|
\mforall{}i,j:nameset(I). ((\muparrow{}isname(f i)) {}\mRightarrow{} (\muparrow{}isname(f j)) {}\mRightarrow{} ((f i) = (f j)) {}\mRightarrow{} (i = j))\}
Date html generated:
2016_05_20-AM-09_29_30
Last ObjectModification:
2015_09_23-AM-09_29_28
Theory : cubical!sets
Home
Index