Library UniMath.CategoryTheory.DisplayedCats.Examples.UnitalBinop

Author: Niels van der Weide Suppose, we have a set `X` with a binary operation `f : X → X → X`. Since init elments for `f` are unique, the type of unit elements of `f` is a proposition. This means we have two ways of defining a univalent category of sets with a unital binary operations: 1. We define it as a full subcategory of the category of sets with a binary operation 2. We use algebras of the signature describing sets with a binary operation and a unit, which satisfy the necessary axioms. Note that in the first category the morphismms are all functions between sets which preserve the binary relation, while the morphisms in the second category must preserve the unit element as well. As a consequence, the forgetful is full and faithful in the first construction, while in the second it is only faithful. On the nLab, there are definitions which describe when functors forget properties and when functors forget stuff. https://ncatlab.org/nlab/show/stuff2C+propertydefinitions With this terminology, we can argue why the first approach adds the unit as a property while in the second approach it is added as structure.

Let us start by defining sets with a binary operation on them. To do so, we use algebras on the diagonal functor. Let us repeat the diagonal. After that, we show we have a univalent category of sets with a binary operation.

In the remainder, we need some projections.

Now we look at two ways of defining a category of sets with a binary operation and a unit. The first way, is by using the full subcategory. This gives rise to a univalent category since unit elements are unique.

To argue that the unit element is really added as a property, we look at the forgetful functor to sets with binary operations. This functor only forgets the unit and, since the unit was added as a property, it is full and faithful. Note that in this displayed category:

• the displayed objects form a proposition
• the displayed morphisms are contractible

Next we show how to define sets with a binary operation and a unit where the unit is added as structure. To do so, we use displayed categories. To prove univalence of the total category, we use displayed univalence.

Some projections of sets with a binary operation and a point.

Up to now, we only added the element which represents the unit. Beside that, we also need to add the necessary laws.

We finish by arguing that the unit is indeed added structure for this construction. To do so, we prove that the forgetful functor is faithful.

We can also show that this forgetful functor isn't full. This is because not every homomorphism between sets with binary operations preserve the unit element. For that, we use the following example.

Now let us look at the hlevels of the displayed objects and morphisms of this displayed category. More specifically, both the type of displayed objects and the type of displayed morphisms form propositions.