### Nuprl Lemma : op-cat-comp

`∀C:SmallCategory. ∀[I,J,K,f,g:Top].  (cat-comp(op-cat(C)) I J K f g ~ cat-comp(C) K J I g f)`

Proof

Definitions occuring in Statement :  op-cat: `op-cat(C)` cat-comp: `cat-comp(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` top: `Top` all: `∀x:A. B[x]` apply: `f a` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` small-category: `SmallCategory` spreadn: spread4 op-cat: `op-cat(C)` top: `Top`
Lemmas referenced :  cat_comp_tuple_lemma top_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality hypothesis axiomSqEquality isectElimination hypothesisEquality because_Cache

Latex:
\mforall{}C:SmallCategory.  \mforall{}[I,J,K,f,g:Top].    (cat-comp(op-cat(C))  I  J  K  f  g  \msim{}  cat-comp(C)  K  J  I  g  f)

Date html generated: 2020_05_20-AM-07_52_14
Last ObjectModification: 2017_10_03-PM-00_29_08

Theory : small!categories

Home Index