## Equivalences

Let us say that an opetope is unary if its source tree consists of a single face. With our convention for depicting arbitrary cells, a general unary cell looks as follows:

Of course, the number of input edges of x (and y) depends on the lower dimensional structure, and is here chosen, arbitrarily, to be three.

As in the case for universal cells, we will use a small decoration to indicate that a cell is an equivalence, in this case, a small circle decorating its target edge like so

With these conventions in mind, the following coinductive definition of an equivalence in a higher category is standard:

Equivalences

Definition: a unary cell f : x → y is said to be an equivalence if there exists g : y → x as well as higher cells η : g ∘ f → id-x and ε : f ∘ g → id-y such that η and ε are equivalences.

Notice how the hypothesis that f be unary assures that it makes sense to speak of a cell g "in the other direction", that is, between the target of f and the source of f, since this diagram remains well formed. It is also readily checked, by symmetry, that g is also an equivalence, though we have not denoted it as such since it is not needed in the definition.

Our goal now is to prove the following:

Proposition

A unary cell is target universal if and only if it is an equivalence.

We think of this proposition as justifying the fact that we can think of target universal cells as the opetopic analog of equivalences or isomorphisms. In the case of a non-unary cell, however, it does not make sense to speak of an inverse. Rather, we must use the universal property as it is given.

### Proof: ⇒

By stability, it suffices to consider that we are given a target universal arrow f.

By the definition of target universality, we obtain a lift in the following diagram:

And we see that, moreover, g is target universal by closure, since id-x is and f is by hypothesis. We pause to note that we have just shown that any target universal unary cell admits an "inverse" which is also target universal. Hence we will freely apply this observation to other unary, target universal cells which we will encounter in the proof.

Continuing with our proof, we can now obtain the desired cell η using the lift

Futhermore, since η is a unary, target universal cell, we conclude that it is an equivalence by the coinductive hypothesis.

The construction of ε is more involved, and proceeds as follows. First, recall that we have already constructed a left unit law for any arrow which, applied to f, has the form.

Similarly, we have the right unit, unit-r. From the first step of the proof, each of these unary, target universal cells has an inverse which we will denote unit-l-inv and unit-r-inv respectively in what follows.

Our first step is to lift f along itself, creating the cell α as shown

Next, we define β as

And φ as

Next use the source lifting property obtained from the definition of α twice, once for φ and once for β, obtaining the cells φ and γ as follows:

We now define ε as the composite

And finally, since ε is a unary, target universal cell, we conclude that it is an equivalence by the coinductive hypothesis.

This completes the proof.

Introduction
Opetopic Categories
Opetopic Category Theory
Opetopes and Type Theory