Given: Rules R Initial finite Quilder Q1 Desired finite Quilder Q2 Search for derivation of Q2 from Q1 using R Defn: a Quilder consists of: A porder P Two sub-porders C and F An equivalence relation W on P Such that lifting holds: o----->o o----->o | __ /| | __ /| c| /| |wf and wc| /| |f v / | v v / | v o----->o o----->o Rules: Decomposition: If A-->B is unmarked, exists C s.t. A-wc->C-f->B If A-->B is unmarked, exists C s.t. A-c->C-wf->B (equiv (in porders): if A-->B is unmarked, exist C,D s.t. A-wc->C-cf->D-wf->B) If A-w->B, exists C s.t. A-wc->C-wf->B Limits: Can add infs and sups of arbitrary subsets of P; C and WC are closed under pushouts, and F and WF under pullbacks. Note subtlety - the fact that an object is an inf/sup is *not* just a property of the given Quilder - so this data should form part of our structure. Note also that we may, after introducing a sup/inf, end up proving that it is isomorphic aka equal to a pre-existing point. Closedness: Given an arrow, spawn a subinstance, add 2 new objects (and 3 arrows) forming a lifting diagram, and try to prove existence of a lifting arrow. If succeed, label the original arrow with c/wc/f/wf as appropriate. Alternatively: we can just add this new structure to our current Quilder, and record the information that the new -wf-> is a 'test arrow' for our potential -c->, i.e. that if ever we obtain a lifting, we should mark it c. Applying rules: A rule produces a Quilder from a given Quilder by applying the rule then closing off to form porders and equiv rels in obv ways. A derivation of Q2 from Q1 consists of applying rules to Q1 to form some super-Quilder of Q2. So Q2 follows from Q1 iff Q2 is a sub-Quilder of the unique finite Quilder generated from Q1 abiding by all the rules. Stupid search algorithm: generate that finite Quilder, take all sub-Quilders. This is pretty damned stupid. Notes on implementing a Quilder as a data structure: Can implement finite porders as "chainmerge" objects - store a chain decomposition, and for each object x for each chain C_i the index of the greatest element of C_i dominated by x. Then comparisons are constant time, and, ju'ocu'i, adding objects and relations are efficient too.