---

Step * of Lemma adjunction-monad_wf

No Annotations
∀[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 |→ G (F (G (F x))) (F x) ((fst(adj)) (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) (functor-comp(F;G) (functor-comp(F;G) (functor-comp(F;G) X))) 
      (functor-comp(F;G) (functor-comp(F;G) X)) 
      (functor-comp(F;G) X) 
      (x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)) (functor-comp(F;G) X)) 
      (x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)) X))
    = (cat-comp(A) (functor-comp(F;G) (functor-comp(F;G) (functor-comp(F;G) X))) 
       (functor-comp(F;G) (functor-comp(F;G) X)) 
       (functor-comp(F;G) X) 
       (functor-comp(F;G) (functor-comp(F;G) (functor-comp(F;G) X)) (functor-comp(F;G) X) 
        (x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)) X)) 
       (x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)) X))
    ∈ (cat-arrow(A) (functor-comp(F;G) (functor-comp(F;G) (functor-comp(F;G) X))) (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) (functor-comp(F;G) X) (functor-comp(F;G) (functor-comp(F;G) X)) (functor-comp(F;G) X) 
      (functor-comp(F;G) X (functor-comp(F;G) X) ((snd(adj)) X)) 
      (x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)) X))
    = (cat-id(A) (functor-comp(F;G) X))
    ∈ (cat-arrow(A) (functor-comp(F;G) X) (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) (functor-comp(F;G) X) (functor-comp(F;G) (functor-comp(F;G) X)) (functor-comp(F;G) X) 
      ((snd(adj)) (functor-comp(F;G) X)) 
      (x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)) X))
    = (cat-id(A) (functor-comp(F;G) X))
    ∈ (cat-arrow(A) (functor-comp(F;G) X) (functor-comp(F;G) X)))

---

Latex:

---

Latex:
No  Annotations
\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