Nuprl Lemma : mk-adjunction_wf

[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) (G (F a)))].
  (mk-adjunction(b.eps[b];a.eta[a]) ∈ -| 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)) 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 


Definitions occuring in Statement :  mk-adjunction: mk-adjunction(b.eps[b];a.eta[a]) counit-unit-adjunction: -| 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: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] member: t ∈ T apply: a lambda: λx.A[x] function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T counit-unit-adjunction: -| G mk-adjunction: mk-adjunction(b.eps[b];a.eta[a]) pi1: fst(t) pi2: snd(t) mk-nat-trans: |→ 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:  Q prop: squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  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

\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)) 
\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 

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

Theory : small!categories

Home Index