### Nuprl Lemma : nat-trans-comp-equation

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

Proof

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

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)].
\mforall{}[A,B:cat-ob(C)].  \mforall{}[g:cat-arrow(C)  A  B].
((cat-comp(D)  (F  A)  (H  A)  (H  B)  (cat-comp(D)  (F  A)  (G  A)  (H  A)  (t1  A)  (t2  A))  (H  A  B  g))
=  (cat-comp(D)  (F  A)  (F  B)  (H  B)  (F  A  B  g)  (cat-comp(D)  (F  B)  (G  B)  (H  B)  (t1  B)  (t2  B))))

Date html generated: 2020_05_20-AM-07_51_48
Last ObjectModification: 2017_01_11-PM-03_50_52

Theory : small!categories

Home Index