---

Step * of Lemma monad-from_wf

∀[Mnd:Monad]. (monad-from(Mnd) ∈ Monad(TypeCat))
BY
{ ((Intro
    THEN (Assert λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A) BY
                (Auto
                 THEN (Assert M-bind(Mnd) ∈ (M-map(Mnd) (M-map(Mnd) x))
                              ⟶ ((M-map(Mnd) x) ⟶ (M-map(Mnd) x))
                              ⟶ (M-map(Mnd) x) BY
                             Auto)
                 THEN Auto))
    )
   THEN Unfold `monad-from` 0
   THEN MemCD
   THEN Try ((RepUR ``type-cat mk-cat nat-trans functor-comp compose`` 0
              THEN (D 0 THENA Auto)
              THEN (FunExt THENA Auto)
              THEN Reduce 0))) }

1
.....implicit subterm..... 
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
⊢ TypeCat ∈ SmallCategory'

2
.....subterm..... T:t
1:n
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
⊢ functor(ob(T) = M-map(Mnd) T;
          arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x))))) ∈ Functor(TypeCat;TypeCat)

3
.....subterm..... T:t
2:n
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
⊢ λx.M-return(Mnd) ∈ nat-trans(TypeCat;TypeCat;1;functor(ob(T) = M-map(Mnd) T;
                                                         arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x))))))

4
.....subterm..... T:t
3:n
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
⊢ λx,z. (M-bind(Mnd) z (λx.x))
  ∈ nat-trans(TypeCat;TypeCat;functor-comp(functor(ob(T) = M-map(Mnd) T;
                                                   arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));
                                           functor(ob(T) = M-map(Mnd) T;
                                                   arrow(X,Y,f) = λz.(M-bind(Mnd) z 
                                                                      (λx.(M-return(Mnd) 
                                                                           (f x))))));functor(ob(T) = M-map(Mnd) T;
                                                                                              arrow(X,Y,f) =
                                                                                               λz.(M-bind(Mnd) z 
                                                                                                   (λx.(M-return(Mnd) 
                                                                                                        (f x))))))

5
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. X : Type
4. x : M-map(Mnd) (M-map(Mnd) (M-map(Mnd) X))
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.x)) (λx.x))
= (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.x))))) (λx.x))
∈ (M-map(Mnd) X)

6
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. X : Type
4. x : M-map(Mnd) X
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-return(Mnd) x)))) (λx.x)) = x ∈ (M-map(Mnd) X)

7
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. X : Type
4. x : M-map(Mnd) X
⊢ (M-bind(Mnd) (M-return(Mnd) x) (λx.x)) = x ∈ (M-map(Mnd) X)

---

Latex:

---

Latex:
\mforall{}[Mnd:Monad].  (monad-from(Mnd)  \mmember{}  Monad(TypeCat))


By

---

Latex:
((Intro
    THEN  (Assert  \mlambda{}x,z.  (M-bind(Mnd)  z  (\mlambda{}x.x))  \mmember{}  A:Type  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  A))  {}\mrightarrow{}  (M-map(Mnd)  A\000C)  BY
                            (Auto
                              THEN  (Assert  M-bind(Mnd)  \mmember{}  (M-map(Mnd)  (M-map(Mnd)  x))
                                                        {}\mrightarrow{}  ((M-map(Mnd)  x)  {}\mrightarrow{}  (M-map(Mnd)  x))
                                                        {}\mrightarrow{}  (M-map(Mnd)  x)  BY
                                                      Auto)
                              THEN  Auto))
    )
  THEN  Unfold  `monad-from`  0
  THEN  MemCD
  THEN  Try  ((RepUR  ``type-cat  mk-cat  nat-trans  functor-comp  compose``  0
                        THEN  (D  0  THENA  Auto)
                        THEN  (FunExt  THENA  Auto)
                        THEN  Reduce  0)))

---

Home Index