Nuprl Definition : array-model-type
array-model-type{i:l}(AType;Val;n) ==
let Mnd = array-monad(AType) in
let Mnd' = array-monad'(AType) in
⋂T:Type. (T ⟶ (M-map(Mnd) T))
× ⋂T,S:Type. ((M-map(Mnd) T) ⟶ (T ⟶ (M-map(Mnd) S)) ⟶ (M-map(Mnd) S))
× ⋂T:Type. (Val ⟶ (M-map(Mnd) T) ⟶ T)
× ℕn ⟶ Val ⟶ (M-map(Mnd) Unit)
× ⋂T:Type. (T ⟶ (M-map(Mnd') T))
× ⋂T,S:Type. ((M-map(Mnd') T) ⟶ (T ⟶ (M-map(Mnd') S)) ⟶ (M-map(Mnd') S))
× ℕn ⟶ (M-map(Mnd') Val)
× ⋂T:Type. ((M-map(Mnd') T) ⟶ (M-map(Mnd) T))
× Type ⟶ Type
× Type ⟶ Type
× (⋂T:Type. ((Arr(AType) ⟶ (T × Arr(AType))) ⟶ Arr(AType) ⟶ T))
Definitions occuring in Statement :
array-monad': array-monad'(AType),
array-monad: array-monad(AType),
Arr: Arr(AType),
M-map: M-map(mnd),
int_seg: {i..j-},
let: let,
unit: Unit,
apply: f a,
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
natural_number: $n,
universe: Type
Definitions occuring in definition :
array-monad: array-monad(AType),
let: let,
array-monad': array-monad'(AType),
unit: Unit,
int_seg: {i..j-},
natural_number: $n,
apply: f a,
M-map: M-map(mnd),
isect: ⋂x:A. B[x],
universe: Type,
product: x:A × B[x],
function: x:A ⟶ B[x],
Arr: Arr(AType)
FDL editor aliases :
array-model-type
Latex:
array-model-type\{i:l\}(AType;Val;n) ==
let Mnd = array-monad(AType) in
let Mnd' = array-monad'(AType) in
\mcap{}T:Type. (T {}\mrightarrow{} (M-map(Mnd) T))
\mtimes{} \mcap{}T,S:Type. ((M-map(Mnd) T) {}\mrightarrow{} (T {}\mrightarrow{} (M-map(Mnd) S)) {}\mrightarrow{} (M-map(Mnd) S))
\mtimes{} \mcap{}T:Type. (Val {}\mrightarrow{} (M-map(Mnd) T) {}\mrightarrow{} T)
\mtimes{} \mBbbN{}n {}\mrightarrow{} Val {}\mrightarrow{} (M-map(Mnd) Unit)
\mtimes{} \mcap{}T:Type. (T {}\mrightarrow{} (M-map(Mnd') T))
\mtimes{} \mcap{}T,S:Type. ((M-map(Mnd') T) {}\mrightarrow{} (T {}\mrightarrow{} (M-map(Mnd') S)) {}\mrightarrow{} (M-map(Mnd') S))
\mtimes{} \mBbbN{}n {}\mrightarrow{} (M-map(Mnd') Val)
\mtimes{} \mcap{}T:Type. ((M-map(Mnd') T) {}\mrightarrow{} (M-map(Mnd) T))
\mtimes{} Type {}\mrightarrow{} Type
\mtimes{} Type {}\mrightarrow{} Type
\mtimes{} (\mcap{}T:Type. ((Arr(AType) {}\mrightarrow{} (T \mtimes{} Arr(AType))) {}\mrightarrow{} Arr(AType) {}\mrightarrow{} T))
Date html generated:
2016_05_15-PM-02_18_06
Last ObjectModification:
2015_09_23-AM-07_38_31
Theory : monads
Home
Index