Nuprl Definition : tuple-recoding
TupleRecoding ==
L:(Type List) ⟶ (L':Type List
× h:tuple-type(L) ⟶ tuple-type(L')
× {j:tuple-type(L') ⟶ tuple-type(L)| ∀s:tuple-type(L). ((j (h s)) = s ∈ tuple-type(L))} )
Definitions occuring in Statement :
tuple-type: tuple-type(L),
list: T List,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
list: T List,
universe: Type,
product: x:A × B[x],
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
equal: s = t ∈ T,
tuple-type: tuple-type(L),
apply: f a
FDL editor aliases :
tuple-recoding
Latex:
TupleRecoding ==
L:(Type List) {}\mrightarrow{} (L':Type List
\mtimes{} h:tuple-type(L) {}\mrightarrow{} tuple-type(L')
\mtimes{} \{j:tuple-type(L') {}\mrightarrow{} tuple-type(L)| \mforall{}s:tuple-type(L). ((j (h s)) = s)\} )
Date html generated:
2016_05_15-PM-05_48_48
Last ObjectModification:
2015_09_23-AM-07_59_11
Theory : general
Home
Index