Nuprl 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) (ob(G) (ob(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 (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)) 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)) 
        ∈ (cat-arrow(B) (ob(F) (ob(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_lambda(x,y,z.t[x; y; z]) 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) 
                                                                                                                                                                    (ob(F)  (ob(G)  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 

Date html generated: 2017_10_05-AM-00_51_52
Last ObjectModification: 2017_07_28-AM-09_20_40

Theory : small!categories

Home Index