---

Step * of Lemma cat-monad_wf

∀[C:SmallCategory]. (Monad(C) ∈ Type)
BY
{ (Intro THEN Unfold `cat-monad` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
1. C : SmallCategory
⊢ T:Functor(C;C) × nat-trans(C;C;1;T) × nat-trans(C;C;functor-comp(T;T);T) ∈ Type

2
.....subterm..... T:t
2:n
1. C : SmallCategory
2. M : T:Functor(C;C) × nat-trans(C;C;1;T) × nat-trans(C;C;functor-comp(T;T);T)
⊢ let T,u,m = M in 
  (∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (u (ob(T) X)) (m X))
     = (cat-id(C) (ob(T) X))
     ∈ (cat-arrow(C) (ob(T) X) (ob(T) X))))
  ∧ (∀X:cat-ob(C)
       ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) X (ob(T) X) (u X)) (m X))
       = (cat-id(C) (ob(T) X))
       ∈ (cat-arrow(C) (ob(T) X) (ob(T) X))))
  ∧ (∀X:cat-ob(C)
       ((cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (m (ob(T) X)) (m X))
       = (cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) 
          (arrow(T) (ob(T) (ob(T) X)) (ob(T) X) (m X)) 
          (m X))
       ∈ (cat-arrow(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) X)))) ∈ Type

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  (Monad(C)  \mmember{}  Type)


By

---

Latex:
(Intro  THEN  Unfold  `cat-monad`  0  THEN  MemCD)

---

Home Index