Constraints

There are several EA constraints which can be implemented and represented graphically using Easik. These constraints include commutative diagrams, sum constraints, product constraints, pullback constraints and equalizer constraints. Defining constraints requires selecting paths in the sketch. This is done by successive ctrl-clicks on composable edges and then clicking Next or Finish as described below. Note that by definition, some entities involved in constraints have rows that are automatically generated. Easik restricts insertion and deletion on such entities.

Warning!

Invalid Interacting Constraints

We cannot guarantee the correctness of interacting constraints. Our implementations make some combinations invalid. Such an example is when a pullback is a sum. The pullback constraint will try to insert into a table that has, due do a sum constraint, had insertions restricted.

Commutative Diagram

A Commutative Diagram

To add a commutative diagram constraint, select Add a Commutative Diagram from the Constraints menu.

Select the first path involved in the commutative diagram. This path should begin with the domain of the commutative diagram and should terminate at the co-domain. Once the path is selected, click Next.

After selecting the first path, the user will then be prompted to select the second path. Once the second path is selected, the user may then choose Next or Finish depending on whether more paths are involved in the commutative diagram constraint, or whether all paths are accounted for. The user will continue to be prompted to add more paths to the commutative diagram until the Finish or Cancel button is pressed. There is no upper bound to how many paths can be involved in a commutative diagram.

Should the commutative diagram requirements be violated, an error will be produced and no path will be built.

After it is created, new paths can be added to the constraint by right clicking over it in the sketch and selecting Add path(s) to constraint. Path selection works as described above.

Sum Constraint

A Sum Constraint

To add a sum constraint to the sketch, select Add Sum Constraint from the Constraints menu. Select the first path involved in the constraint. This path should begin at a summand and end at the sum. Confirm this path by pressing the Next button at the bottom of the window.

After selecting the first path, the user will then be prompted to select the second path. Once the second path is selected, the user may then choose Next or Finish depending on whether more paths are involved in the sum constraint, or whether all paths are accounted for. The user will continue to be prompted to add more paths to the sum constraint until the Finish or Cancel button is pressed. There is no upper bound to how many paths can be involved in a sum constraint.

There are several conditions which must be observed for the successful creation of a sum constraint:

Should these conditions not be met, an error message will appear, and the constraint will not be created.

After it is created, new paths can be added to the constraint by right clicking over it in the sketch and selecting Add path(s) to constraint. Path selection works as described above.

Product Constraint

A Product Constraint

To add a product constraint to the sketch, select Add Product Constraint from the Constraints menu. The user will then be prompted to select the first path involved in the constraint, and confirm this path by pressing the Next button at the bottom of the sketch pane.

After selecting the first path, the user will then be prompted to select the second path. Once the second path is selected, the user may then choose Next or Finish depending on whether more paths are involved in the product constraint, or whether all paths are accounted for. The user will continue to be prompted to add more paths to the product constraint until the Finish or Cancel button is pressed. There is no upper bound to how many paths can be involved in a product constraint.

There are several conditions which must be observed for the successful addition of a product constraint:

Should these conditions not be met, an error message will appear.

After it is created, new paths can be added to the constraint by right clicking over it in the sketch and selecting Add path(s) to constraint. Path selection works as described above.

Pullback Constraint

A Pullback Constraint

To add a pullback constraint to the sketch, select Add a Pullback Constraintfrom the Constraints menu. The user then defines the paths involved in the pullback constraint. The paths must be selected in the correct order.

The first and second paths must have a common codomain, the codomain of the pullback. The third path must have the pullback entity as its domain and its codomain must be the domain of the first selected path. The fourth path has the pullback entity as its domain and its codomain must be the domain of the second selected path. After the fourth path is selected, click Finish.

There are several conditions which must be observed for the successful addition of a pullback constraint:

Should these conditions not be met, an error message will appear, and the constraint will not be created.

Equalizer Constraint

An Equalizer Constraint

To add an equalizer constraint to the sketch, select Add Equalizer Constraint from the Constraints menu. The user will then be prompted to select the first path involved in the constraint. This path must be a single injective edge that has the equalizer entity as its domain. Confirm this selection by pressing the Next button at the bottom of the window.

After selecting the first path, the user will then be prompted to select the second path. Its domain must be the codomain of the first path. A third path with the same domain and codomain as the second path must be selected, and the user may then choose Next or Finish depending on whether more paths are involved in the equalizer constraint, or whether all paths are accounted for. The user will continue to be prompted to add more paths to the equalizer constraint until the Finish or Cancel button is pressed. There is no upper bound to how many paths can be involved in a equalizer constraint.

There are several conditions which must be observed for the successful addition of an equalizer constraint:

Should these conditions not be met, an error message will appear, and the constraint will not be created.

Adding Paths

Some constraints support path addition after their creation. These include commutative diagrams, product constraints, and sum constraints. To add one or more paths to a constraint, right click on its node and select Add path(s) to constraint from the popup menu. Paths can then be selected by successive ctrl-clicks on composable edges and clicking either next to select another path, or finish to add the selected paths to the constraint.