---

Step * of Lemma mk-adjunction_wf

∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[eps:b:cat-ob(B) ⟶ (cat-arrow(B) (ob(F) (ob(G) b)) b)].
∀[eta:a:cat-ob(A) ⟶ (cat-arrow(A) a (ob(G) (ob(F) a)))].
  (mk-adjunction(b.eps[b];a.eta[a]) ∈ F -| G) supposing 
     ((∀a1,a2:cat-ob(A). ∀g:cat-arrow(A) a1 a2.
         ((cat-comp(A) a1 (ob(G) (ob(F) a1)) (ob(G) (ob(F) a2)) eta[a1] 
           (arrow(G) (ob(F) a1) (ob(F) a2) (arrow(F) a1 a2 g)))
         = (cat-comp(A) a1 a2 (ob(G) (ob(F) a2)) g eta[a2])
         ∈ (cat-arrow(A) a1 (ob(G) (ob(F) a2))))) and 
     (∀b1,b2:cat-ob(B). ∀g:cat-arrow(B) b1 b2.
        ((cat-comp(B) (ob(F) (ob(G) b1)) b1 b2 eps[b1] g)
        = (cat-comp(B) (ob(F) (ob(G) b1)) (ob(F) (ob(G) b2)) b2 (arrow(F) (ob(G) b1) (ob(G) b2) (arrow(G) b1 b2 g)) 
           eps[b2])
        ∈ (cat-arrow(B) (ob(F) (ob(G) b1)) b2))) and 
     counit-unit-equations(A;B;F;G;λb.eps[b];λa.eta[a]))
BY
{ (((Intros THEN MemTypeCD THEN Try ((RepUR ``mk-adjunction mk-nat-trans`` 0 THEN Trivial)))
    THENW (D -1 THEN D -2 THEN D -1 THEN All (RepUR  ``functor-comp id_functor``) THEN Auto)
    )
   THEN RepUR ``mk-adjunction`` 0
   THEN RepeatFor 2 (MemCD)
   THEN All (RepUR  ``functor-comp id_functor``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;A)].  \mforall{}[eps:b:cat-ob(B)  {}\mrightarrow{}  (cat-arrow(B) 
                                                                                                                                                                    (ob(F)  (ob(G)  b)) 
                                                                                                                                                                    b)].
\mforall{}[eta:a:cat-ob(A)  {}\mrightarrow{}  (cat-arrow(A)  a  (ob(G)  (ob(F)  a)))].
    (mk-adjunction(b.eps[b];a.eta[a])  \mmember{}  F  -|  G)  supposing 
          ((\mforall{}a1,a2:cat-ob(A).  \mforall{}g:cat-arrow(A)  a1  a2.
                  ((cat-comp(A)  a1  (ob(G)  (ob(F)  a1))  (ob(G)  (ob(F)  a2))  eta[a1] 
                      (arrow(G)  (ob(F)  a1)  (ob(F)  a2)  (arrow(F)  a1  a2  g)))
                  =  (cat-comp(A)  a1  a2  (ob(G)  (ob(F)  a2))  g  eta[a2])))  and 
          (\mforall{}b1,b2:cat-ob(B).  \mforall{}g:cat-arrow(B)  b1  b2.
                ((cat-comp(B)  (ob(F)  (ob(G)  b1))  b1  b2  eps[b1]  g)
                =  (cat-comp(B)  (ob(F)  (ob(G)  b1))  (ob(F)  (ob(G)  b2))  b2 
                      (arrow(F)  (ob(G)  b1)  (ob(G)  b2)  (arrow(G)  b1  b2  g)) 
                      eps[b2])))  and 
          counit-unit-equations(A;B;F;G;\mlambda{}b.eps[b];\mlambda{}a.eta[a]))


By

---

Latex:
(((Intros  THEN  MemTypeCD  THEN  Try  ((RepUR  ``mk-adjunction  mk-nat-trans``  0  THEN  Trivial)))
    THENW  (D  -1  THEN  D  -2  THEN  D  -1  THEN  All  (RepUR    ``functor-comp  id\_functor``)  THEN  Auto)
    )
  THEN  RepUR  ``mk-adjunction``  0
  THEN  RepeatFor  2  (MemCD)
  THEN  All  (RepUR    ``functor-comp  id\_functor``)
  THEN  Auto)

---

Home Index