Nuprl Lemma : functor-comp_wf

[A,B,C:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;C)].  (functor-comp(F;G) ∈ Functor(A;C))


Proof




Definitions occuring in Statement :  functor-comp: functor-comp(F;G) cat-functor: Functor(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T functor-comp: functor-comp(F;G) so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] uimplies: supposing a all: x:A. B[x] squash: T prop: true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  mk-functor_wf functor-ob_wf cat-ob_wf functor-arrow_wf cat-arrow_wf equal_wf squash_wf true_wf functor-arrow-comp cat-comp_wf iff_weakening_equal functor-arrow-id cat-id_wf cat-functor_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality applyEquality because_Cache hypothesis independent_isectElimination lambdaFormation imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination dependent_functionElimination axiomEquality isect_memberEquality

Latex:
\mforall{}[A,B,C:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;C)].    (functor-comp(F;G)  \mmember{}  Functor(A;C))



Date html generated: 2017_10_05-AM-00_47_23
Last ObjectModification: 2017_07_28-AM-09_19_40

Theory : small!categories


Home Index