### Nuprl Lemma : nat-trans-equation

`∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[T:nat-trans(C;D;F;G)]. ∀[A,B:cat-ob(C)]. ∀[g:cat-arrow(C) A B].`
`  ((cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(G) B) (T A) (functor-arrow(G) A B g))`
`  = (cat-comp(D) (functor-ob(F) A) (functor-ob(F) B) (functor-ob(G) B) (functor-arrow(F) A B g) (T B))`
`  ∈ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) B)))`

Proof

Definitions occuring in Statement :  nat-trans: `nat-trans(C;D;F;G)` functor-arrow: `functor-arrow(F)` functor-ob: `functor-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` uall: `∀[x:A]. B[x]` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` nat-trans: `nat-trans(C;D;F;G)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  small-category_wf cat-functor_wf nat-trans_wf cat-ob_wf cat-arrow_wf
Rules used in proof :  because_Cache axiomEquality isect_memberEquality sqequalRule isectElimination extract_by_obid applyEquality hypothesisEquality dependent_functionElimination hypothesis rename thin setElimination sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F,G:Functor(C;D)].  \mforall{}[T:nat-trans(C;D;F;G)].  \mforall{}[A,B:cat-ob(C)].
\mforall{}[g:cat-arrow(C)  A  B].
((cat-comp(D)  (functor-ob(F)  A)  (functor-ob(G)  A)  (functor-ob(G)  B)  (T  A)
(functor-arrow(G)  A  B  g))
=  (cat-comp(D)  (functor-ob(F)  A)  (functor-ob(F)  B)  (functor-ob(G)  B)  (functor-arrow(F)  A  B  g)
(T  B)))

Date html generated: 2017_01_11-AM-09_18_01
Last ObjectModification: 2017_01_10-PM-00_07_17

Theory : small!categories

Home Index