---

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) (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
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)  (ob(T)  X)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (u  (ob(T)  X))  (m  X))
          =  (cat-id(C)  (ob(T)  X))))
    \mwedge{}  (\mforall{}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))))
    \mwedge{}  (\mforall{}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))))  \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