### Nuprl Lemma : counit-unit-equations_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)))].
(counit-unit-equations(A;B;F;G;eps;eta) ∈ ℙ)

Proof

Definitions occuring in Statement :  counit-unit-equations: counit-unit-equations(D;C;F;G;eps;eta) functor-ob: ob(F) cat-functor: Functor(C1;C2) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] prop: member: t ∈ T apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T counit-unit-equations: counit-unit-equations(D;C;F;G;eps;eta) prop: and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x]
Lemmas referenced :  all_wf cat-ob_wf equal_wf cat-arrow_wf functor-ob_wf cat-comp_wf functor-arrow_wf cat-id_wf cat-functor_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality applyEquality because_Cache functionExtensionality axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality

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)))].
(counit-unit-equations(A;B;F;G;eps;eta)  \mmember{}  \mBbbP{})

Date html generated: 2017_01_19-PM-02_57_20
Last ObjectModification: 2017_01_16-PM-00_19_09

Theory : small!categories

Home Index