Nuprl Definition : type-recoding
TypeRecoding == T:Type ⟶ (L:Type List × h:T ⟶ tuple-type(L) × {j:tuple-type(L) ⟶ T| ∀s:T. ((j (h s)) = s ∈ T)} )
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],
tuple-type: tuple-type(L),
all: ∀x:A. B[x],
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
type-recoding
Latex:
TypeRecoding ==
T:Type {}\mrightarrow{} (L:Type List \mtimes{} h:T {}\mrightarrow{} tuple-type(L) \mtimes{} \{j:tuple-type(L) {}\mrightarrow{} T| \mforall{}s:T. ((j (h s)) = s)\} )
Date html generated:
2016_05_15-PM-05_48_29
Last ObjectModification:
2015_09_23-AM-07_59_02
Theory : general
Home
Index