Nuprl Lemma : identity-trans_wf

[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (identity-trans(C;D;F) ∈ nat-trans(C;D;F;F))


Proof




Definitions occuring in Statement :  identity-trans: identity-trans(C;D;F) 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 identity-trans: identity-trans(C;D;F) so_lambda: λ2x.t[x] so_apply: x[s] 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-nat-trans_wf cat-id_wf functor-ob_wf cat-ob_wf equal_wf squash_wf true_wf cat-arrow_wf cat-comp-ident1 functor-arrow_wf cat-comp_wf iff_weakening_equal cat-comp-ident2 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 because_Cache lambdaEquality applyEquality hypothesis independent_isectElimination lambdaFormation imageElimination equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination axiomEquality isect_memberEquality

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].    (identity-trans(C;D;F)  \mmember{}  nat-trans(C;D;F;F))



Date html generated: 2020_05_20-AM-07_51_35
Last ObjectModification: 2017_07_28-AM-09_19_19

Theory : small!categories


Home Index