### Nuprl Lemma : functor-arrow-prod-id

`∀[A,B,C:SmallCategory]. ∀[F:Functor(A × B;C)]. ∀[a:cat-ob(A)]. ∀[b:cat-ob(B)].`
`  ((F <a, b> <a, b> <cat-id(A) a, cat-id(B) b>) = (cat-id(C) (F <a, b>)) ∈ (cat-arrow(C) (F <a, b>) (F <a, b>)))`

Proof

Definitions occuring in Statement :  product-cat: `A × B` functor-arrow: `arrow(F)` functor-ob: `ob(F)` cat-functor: `Functor(C1;C2)` cat-id: `cat-id(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` apply: `f a` pair: `<a, b>` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` cat-ob: `cat-ob(C)` pi1: `fst(t)` product-cat: `A × B` pi2: `snd(t)`
Lemmas referenced :  functor-arrow-id product-cat_wf cat-ob_wf cat-functor_wf small-category_wf id_prod_cat_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_functionElimination sqequalRule independent_pairEquality universeIsType isect_memberEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType Error :memTop

Latex:
\mforall{}[A,B,C:SmallCategory].  \mforall{}[F:Functor(A  \mtimes{}  B;C)].  \mforall{}[a:cat-ob(A)].  \mforall{}[b:cat-ob(B)].
((F  <a,  b>  <a,  b>  <cat-id(A)  a,  cat-id(B)  b>)  =  (cat-id(C)  (F  <a,  b>)))

Date html generated: 2020_05_20-AM-07_54_15
Last ObjectModification: 2019_12_30-PM-03_22_13

Theory : small!categories

Home Index