Nuprl Lemma : groupoid-square2_wf

G:Groupoid. ∀x00,x10,x01,x11:cat-ob(cat(G)). ∀d:cat-arrow(cat(G)) x01 x11. ∀b:cat-arrow(cat(G)) x10 x11.
c:cat-arrow(cat(G)) x00 x01.
  (groupoid-square2(G;x00;x10;x01;x11;b;c;d) ∈ {a:cat-arrow(cat(G)) x00 x10| d} )


Proof




Definitions occuring in Statement :  groupoid-square2: groupoid-square2(G;x00;x10;x01;x11;b;c;d) groupoid-cat: cat(G) groupoid: Groupoid cat-square-commutes: x_y1 y1_z x_y2 y2_z cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) all: x:A. B[x] member: t ∈ T set: {x:A| B[x]}  apply: a
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T groupoid-square2: groupoid-square2(G;x00;x10;x01;x11;b;c;d) uall: [x:A]. B[x] cat-square-commutes: x_y1 y1_z x_y2 y2_z prop: true: True implies:  Q squash: T and: P ∧ Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a
Lemmas referenced :  groupoid-left-cancellation cat-comp-ident groupoid_inv cat-comp-assoc true_wf squash_wf uiff_transitivity3 cat-id_wf equal_wf groupoid_wf cat-ob_wf cat-arrow_wf cat-square-commutes_wf groupoid-inv_wf groupoid-cat_wf cat-comp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule dependent_set_memberEquality applyEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache natural_numberEquality independent_functionElimination lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination productElimination imageMemberEquality baseClosed independent_isectElimination

Latex:
\mforall{}G:Groupoid.  \mforall{}x00,x10,x01,x11:cat-ob(cat(G)).  \mforall{}d:cat-arrow(cat(G))  x01  x11.
\mforall{}b:cat-arrow(cat(G))  x10  x11.  \mforall{}c:cat-arrow(cat(G))  x00  x01.
    (groupoid-square2(G;x00;x10;x01;x11;b;c;d)  \mmember{}  \{a:cat-arrow(cat(G))  x00  x10|  a  o  b  =  c  o  d\}  )



Date html generated: 2016_05_18-AM-11_56_10
Last ObjectModification: 2016_01_17-PM-02_16_54

Theory : small!categories


Home Index