---

Step * of Lemma cat-monad_wf

No Annotations
∀[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) (T X) (T (T X)) (T X) (u (T X)) (m X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
  ∧ (∀X:cat-ob(C)
       ((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (u X)) (m X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
  ∧ (∀X:cat-ob(C)
       ((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (m (T X)) (m X))
       = (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (m X)) (m X))
       ∈ (cat-arrow(C) (T (T (T X))) (T X)))) ∈ Type

---

Latex:

---

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


By

---

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

---

Home Index