### Nuprl Lemma : cat-comp-isomorphism

`∀C:SmallCategory. ∀a,b,c:cat-ob(C). ∀f:cat-arrow(C) a b. ∀g:cat-arrow(C) b c.`
`  (cat-isomorphism(C;a;b;f) `` cat-isomorphism(C;b;c;g) `` cat-isomorphism(C;a;c;cat-comp(C) a b c f g))`

Proof

Definitions occuring in Statement :  cat-isomorphism: `cat-isomorphism(C;x;y;f)` cat-comp: `cat-comp(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` cat-isomorphism: `cat-isomorphism(C;x;y;f)` exists: `∃x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` cand: `A c∧ B` cat-inverse: `fg=1` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  cat-isomorphism_wf cat-arrow_wf cat-ob_wf small-category_wf cat-comp_wf cat-inverse_wf equal_wf iff_weakening_equal cat-comp-ident2 squash_wf true_wf cat-comp-assoc cat-comp-ident1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin rename cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis applyEquality dependent_pairFormation independent_pairFormation productEquality equalityUniverse levelHypothesis equalityTransitivity equalitySymmetry natural_numberEquality because_Cache lambdaEquality imageElimination sqequalRule imageMemberEquality baseClosed independent_isectElimination independent_functionElimination dependent_functionElimination universeEquality

Latex:
\mforall{}C:SmallCategory.  \mforall{}a,b,c:cat-ob(C).  \mforall{}f:cat-arrow(C)  a  b.  \mforall{}g:cat-arrow(C)  b  c.
(cat-isomorphism(C;a;b;f)
{}\mRightarrow{}  cat-isomorphism(C;b;c;g)
{}\mRightarrow{}  cat-isomorphism(C;a;c;cat-comp(C)  a  b  c  f  g))

Date html generated: 2020_05_20-AM-07_50_12
Last ObjectModification: 2017_07_28-AM-09_19_04

Theory : small!categories

Home Index