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

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

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` function: `x:A ⟶ B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat-trans: `nat-trans(C;D;F;G)` true: `True` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  cat-ob_wf cat-arrow_wf nat-trans_wf cat-functor_wf small-category_wf functor-ob_wf cat-comp_wf functor-arrow_wf equal_wf squash_wf true_wf istype-universe functor-arrow-comp subtype_rel_self iff_weakening_equal nat-trans-equation
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut hypothesis universeIsType introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality because_Cache inhabitedIsType functionEquality setElimination rename natural_numberEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry instantiate universeEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination

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

Date html generated: 2020_05_20-AM-07_51_23
Last ObjectModification: 2019_12_30-PM-02_08_16

Theory : small!categories

Home Index