`∀[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]))`

Proof

Definitions occuring in Statement :  mk-adjunction: `mk-adjunction(b.eps[b];a.eta[a])` counit-unit-adjunction: `F -| G` counit-unit-equations: `counit-unit-equations(D;C;F;G;eps;eta)` functor-arrow: `arrow(F)` functor-ob: `ob(F)` cat-functor: `Functor(C1;C2)` cat-comp: `cat-comp(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` counit-unit-adjunction: `F -| G` mk-adjunction: `mk-adjunction(b.eps[b];a.eta[a])` pi1: `fst(t)` pi2: `snd(t)` mk-nat-trans: `x |→ T[x]` nat-trans: `nat-trans(C;D;F;G)` id_functor: `1` functor-comp: `functor-comp(F;G)` all: `∀x:A. B[x]` top: `Top` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` prop: `ℙ` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  ob_mk_functor_lemma arrow_mk_functor_lemma counit-unit-equations_wf cat-ob_wf cat-arrow_wf functor-ob_wf pi1_wf_top equal_wf all_wf cat-comp_wf functor-arrow_wf cat-functor_wf small-category_wf mk-functor_wf squash_wf true_wf functor-arrow-comp iff_weakening_equal functor-arrow-id cat-id_wf mk-nat-trans_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation dependent_set_memberEquality sqequalRule hypothesis productElimination thin sqequalHypSubstitution setElimination rename cut introduction extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality isectElimination hypothesisEquality independent_pairEquality functionExtensionality applyEquality productEquality functionEquality lambdaFormation equalityTransitivity equalitySymmetry independent_functionElimination because_Cache lambdaEquality independent_isectElimination imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed

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)
(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]))

Date html generated: 2020_05_20-AM-07_58_21
Last ObjectModification: 2017_07_28-AM-09_20_40

Theory : small!categories

Home Index