---

Step * of Lemma mk-adjunction_wf

No Annotations
∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[eps:b:cat-ob(B) ⟶ (cat-arrow(B) (F (G b)) b)].
∀[eta:a:cat-ob(A) ⟶ (cat-arrow(A) a (G (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 (G (F a1)) (G (F a2)) eta[a1] (G (F a1) (F a2) (F a1 a2 g)))
         = (cat-comp(A) a1 a2 (G (F a2)) g eta[a2])
         ∈ (cat-arrow(A) a1 (G (F a2))))) and 
     (∀b1,b2:cat-ob(B). ∀g:cat-arrow(B) b1 b2.
        ((cat-comp(B) (F (G b1)) b1 b2 eps[b1] g)
        = (cat-comp(B) (F (G b1)) (F (G b2)) b2 (F (G b1) (G b2) (G b1 b2 g)) eps[b2])
        ∈ (cat-arrow(B) (F (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:
No  Annotations
\mforall{}[A,B:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;A)].  \mforall{}[eps:b:cat-ob(B)  {}\mrightarrow{}  (cat-arrow(B) 
                                                                                                                                                                    (F  (G  b)) 
                                                                                                                                                                    b)].
\mforall{}[eta:a:cat-ob(A)  {}\mrightarrow{}  (cat-arrow(A)  a  (G  (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  (G  (F  a1))  (G  (F  a2))  eta[a1]  (G  (F  a1)  (F  a2)  (F  a1  a2  g)))
                  =  (cat-comp(A)  a1  a2  (G  (F  a2))  g  eta[a2])))  and 
          (\mforall{}b1,b2:cat-ob(B).  \mforall{}g:cat-arrow(B)  b1  b2.
                ((cat-comp(B)  (F  (G  b1))  b1  b2  eps[b1]  g)
                =  (cat-comp(B)  (F  (G  b1))  (F  (G  b2))  b2  (F  (G  b1)  (G  b2)  (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