---

Step * of Lemma adjunction-monad_wf

∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[adj:F -| G].  (adjMonad(adj) ∈ Monad(A))
BY
{ (Intros THEN Unfold `adjunction-monad` 0 THEN MemCD THEN Try (QuickAuto)) }

1
.....subterm..... T:t
3:n
1. A : SmallCategory
2. B : SmallCategory
3. F : Functor(A;B)
4. G : Functor(B;A)
5. adj : F -| G
⊢ x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x))
  ∈ nat-trans(A;A;functor-comp(functor-comp(F;G);functor-comp(F;G));functor-comp(F;G))

2
1. A : SmallCategory
2. B : SmallCategory
3. F : Functor(A;B)
4. G : Functor(B;A)
5. adj : F -| G
⊢ ∀X:cat-ob(A)
    ((cat-comp(A) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X))) 
      (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X)) 
      (ob(functor-comp(F;G)) X) 
      (x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)) (ob(functor-comp(F;G)) X)) 
      (x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)) X))
    = (cat-comp(A) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X))) 
       (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X)) 
       (ob(functor-comp(F;G)) X) 
       (arrow(functor-comp(F;G)) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X)) (ob(functor-comp(F;G)) X) 
        (x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)) X)) 
       (x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)) X))
    ∈ (cat-arrow(A) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X))) 
       (ob(functor-comp(F;G)) X)))

3
1. A : SmallCategory
2. B : SmallCategory
3. F : Functor(A;B)
4. G : Functor(B;A)
5. adj : F -| G
⊢ ∀X:cat-ob(A)
    ((cat-comp(A) (ob(functor-comp(F;G)) X) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X)) (ob(functor-comp(F;G)) X) 
      (arrow(functor-comp(F;G)) X (ob(functor-comp(F;G)) X) ((snd(adj)) X)) 
      (x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)) X))
    = (cat-id(A) (ob(functor-comp(F;G)) X))
    ∈ (cat-arrow(A) (ob(functor-comp(F;G)) X) (ob(functor-comp(F;G)) X)))

4
1. A : SmallCategory
2. B : SmallCategory
3. F : Functor(A;B)
4. G : Functor(B;A)
5. adj : F -| G
⊢ ∀X:cat-ob(A)
    ((cat-comp(A) (ob(functor-comp(F;G)) X) (ob(functor-comp(F;G)) (ob(functor-comp(F;G)) X)) (ob(functor-comp(F;G)) X) 
      ((snd(adj)) (ob(functor-comp(F;G)) X)) 
      (x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)) X))
    = (cat-id(A) (ob(functor-comp(F;G)) X))
    ∈ (cat-arrow(A) (ob(functor-comp(F;G)) X) (ob(functor-comp(F;G)) X)))

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;A)].  \mforall{}[adj:F  -|  G].
    (adjMonad(adj)  \mmember{}  Monad(A))


By

---

Latex:
(Intros  THEN  Unfold  `adjunction-monad`  0  THEN  MemCD  THEN  Try  (QuickAuto))

---

Home Index