Nuprl Lemma : trans-comp_wf

[C,D:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[t1:nat-trans(C;D;F;G)]. ∀[t2:nat-trans(C;D;G;H)].
  (t1 t2 ∈ nat-trans(C;D;F;H))


Proof




Definitions occuring in Statement :  trans-comp: t1 t2 nat-trans: nat-trans(C;D;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 trans-comp: t1 t2 so_lambda: λ2x.t[x] nat-trans: nat-trans(C;D;F;G) so_apply: x[s] uimplies: supposing a all: x:A. B[x] true: True squash: T prop: subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  mk-nat-trans_wf cat-comp_wf functor-ob_wf cat-ob_wf cat-arrow_wf nat-trans_wf cat-functor_wf small-category_wf functor-arrow_wf equal_wf squash_wf true_wf cat-comp-assoc nat-trans-equation iff_weakening_equal
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 setElimination rename independent_isectElimination lambdaFormation axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality natural_numberEquality imageElimination universeEquality dependent_functionElimination imageMemberEquality baseClosed productElimination independent_functionElimination

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F,G,H:Functor(C;D)].  \mforall{}[t1:nat-trans(C;D;F;G)].  \mforall{}[t2:nat-trans(C;D;G;H)].
    (t1  o  t2  \mmember{}  nat-trans(C;D;F;H))



Date html generated: 2017_10_05-AM-00_46_14
Last ObjectModification: 2017_07_28-AM-09_19_21

Theory : small!categories


Home Index