---

Step * 2 of Lemma cat-monad_wf

.....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
BY
{ ((RepeatFor 2 (D -1) THEN Reduce 0) THEN (D -2 THEN D -1 THEN All (RepUR  ``functor-comp id_functor``)) THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  C  :  SmallCategory
2.  M  :  T:Functor(C;C)  \mtimes{}  nat-trans(C;C;1;T)  \mtimes{}  nat-trans(C;C;functor-comp(T;T);T)
\mvdash{}  let  T,u,m  =  M  in 
    (\mforall{}X:cat-ob(C).  ((cat-comp(C)  (T  X)  (T  (T  X))  (T  X)  (u  (T  X))  (m  X))  =  (cat-id(C)  (T  X))))
    \mwedge{}  (\mforall{}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))))
    \mwedge{}  (\mforall{}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))))  \mmember{}  Type


By

---

Latex:
((RepeatFor  2  (D  -1)  THEN  Reduce  0)
  THEN  (D  -2  THEN  D  -1  THEN  All  (RepUR    ``functor-comp  id\_functor``))
  THEN  Auto)

---

Home Index