Nuprl Lemma : A-bind_wf

[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type].
  (A-bind(array-model(AType)) ∈ (A-map T) ⟶ (T ⟶ (A-map S)) ⟶ (A-map S))


Proof




Definitions occuring in Statement :  A-bind: A-bind(AModel) A-map: A-map array-model: array-model(AType) array: array{i:l}(Val;n) nat: uall: [x:A]. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] array-model: array-model(AType) A-bind: A-bind(AModel) A-map: A-map pi2: snd(t) pi1: fst(t) array-monad: array-monad(AType) M-bind: M-bind(Mnd) M-map: M-map(mnd) let: let mk_monad: mk_monad(M;return;bind) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  array_wf nat_wf pi1_wf Arr_wf pi2_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity universeEquality because_Cache cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis isect_memberFormation introduction sqequalRule axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality lambdaEquality applyEquality functionEquality productEquality

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].  \mforall{}[T,S:Type].
    (A-bind(array-model(AType))  \mmember{}  (A-map  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (A-map  S))  {}\mrightarrow{}  (A-map  S))



Date html generated: 2016_05_15-PM-02_18_28
Last ObjectModification: 2015_12_27-AM-08_58_51

Theory : monads


Home Index