## Universal Properties

One of the attractive features of working with opetopic categories is that the very definition of an opetopic category is given in terms of what is possibly the most important concept of category theory: universal properties.

In this section, we are going to describe two universal properties that a cell in an opetopic set might have. The definitions are mutually coinductive, but we hope this will not scare away too many readers.

Let's begin with a cell f as in the previous section.

We will first introduce notation for the properties we are interested in, and then explain what that notation means. The first property is called target universality, and a cell which is target universal will be denoted with a small triangle decorating the output edge corresponding to its target as follows:

The second universal property we will be interested in is called source universality and depends on the choice of a particular source cell of f. It will similarly be denoted by a small triangle, this time decorating the appropriate input edge:

In the above diagram, we have labelled the input edges with the faces they correspond in order to aid the reader in seeing what assertion is being made about f by the decoration: by decorating the edge corresponding to the cell x, we mean to assert that f is source universal at x.

We now proceed to the definitions.

Target Universal

Definition: a cell f is said to be target universal if for all s and t filling the cells depicted in green, there exist u and v completing the diagram such that v both is target universal and source universal at u.

Let us pause to make a couple remarks before moving on to the definition of source universal. First of all, the observant reader will notice that the shape depicted in the diagram above is exactly the target extrusion of f as discussed in the previous section. We have colored the cells in the diagram simply as a means to aid the reader in recognizing what are the hypotheses of the definition (in green), and what are its conclusions (in red).

We now finish the definition by explaining what it is for a cell f to be source universal at a chosen source cell x. Not surprisingly this definition will make use of the source extrusion at x.

Source Universal

Definition: a cell f is said to be source universal at a given source cell x if for all s and t filling the cells depicted in green, there exist u and v completing the diagram such that v is both target universal and source universal at u.

With these two concepts in hand, we can now proceed to the definition of an opetopic category.

Introduction
Opetopic Categories
Opetopic Category Theory
Opetopes and Type Theory