Nuprl Lemma : mk-cat_wf

[ob:Type]. ∀[arrow:ob ⟶ ob ⟶ Type]. ∀[id:x:ob ⟶ arrow[x;x]]. ∀[comp:x:ob
                                                                        ⟶ y:ob
                                                                        ⟶ z:ob
                                                                        ⟶ arrow[x;y]
                                                                        ⟶ arrow[y;z]
                                                                        ⟶ arrow[x;z]].
  (Cat(ob ob;
       arrow(x,y) arrow[x;y];
       id(a) id[a];
       comp(u,v,w,f,g) comp[u;v;w;f;g]) ∈ SmallCategory) supposing 
     ((∀x,y,z,w:ob. ∀f:arrow[x;y]. ∀g:arrow[y;z]. ∀h:arrow[z;w].
         (comp[x;z;w;comp[x;y;z;f;g];h] comp[x;y;w;f;comp[y;z;w;g;h]] ∈ arrow[x;w])) and 
     (∀x,y:ob. ∀f:arrow[x;y].  ((comp[x;x;y;id[x];f] f ∈ arrow[x;y]) ∧ (comp[x;y;y;f;id[y]] f ∈ arrow[x;y]))))


Definitions occuring in Statement :  mk-cat: mk-cat small-category: SmallCategory uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2;s3;s4;s5] so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] and: P ∧ Q member: t ∈ T function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a small-category: SmallCategory mk-cat: mk-cat so_apply: x[s1;s2;s3;s4;s5] so_apply: x[s] so_apply: x[s1;s2] subtype_rel: A ⊆B spreadn: spread4 and: P ∧ Q so_lambda: λ2x.t[x] prop: all: x:A. B[x]
Lemmas referenced :  all_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality sqequalRule dependent_pairEquality because_Cache lambdaEquality applyEquality functionExtensionality hypothesisEquality independent_pairEquality hypothesis sqequalHypSubstitution productEquality functionEquality thin cumulativity universeEquality independent_pairFormation productElimination extract_by_obid isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

\mforall{}[ob:Type].  \mforall{}[arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type].  \mforall{}[id:x:ob  {}\mrightarrow{}  arrow[x;x]].  \mforall{}[comp:x:ob
                                                                                                                                                {}\mrightarrow{}  y:ob
                                                                                                                                                {}\mrightarrow{}  z:ob
                                                                                                                                                {}\mrightarrow{}  arrow[x;y]
                                                                                                                                                {}\mrightarrow{}  arrow[y;z]
                                                                                                                                                {}\mrightarrow{}  arrow[x;z]].
    (Cat(ob  =  ob;
              arrow(x,y)  =  arrow[x;y];
              id(a)  =  id[a];
              comp(u,v,w,f,g)  =  comp[u;v;w;f;g])  \mmember{}  SmallCategory)  supposing 
          ((\mforall{}x,y,z,w:ob.  \mforall{}f:arrow[x;y].  \mforall{}g:arrow[y;z].  \mforall{}h:arrow[z;w].
                  (comp[x;z;w;comp[x;y;z;f;g];h]  =  comp[x;y;w;f;comp[y;z;w;g;h]]))  and 
          (\mforall{}x,y:ob.  \mforall{}f:arrow[x;y].    ((comp[x;x;y;id[x];f]  =  f)  \mwedge{}  (comp[x;y;y;f;id[y]]  =  f))))

Date html generated: 2020_05_20-AM-07_49_42
Last ObjectModification: 2017_07_28-AM-09_18_56

Theory : small!categories

Home Index