## Stream: maths

### Topic: units and is_unit

#### Scott Morrison (Sep 12 2019 at 22:17):

Are we happy with the design of units and is_unit?

structure units (α : Type u) [monoid α] :=
(val : α)
(inv : α)
(val_inv : val * inv = 1)
(inv_val : inv * val = 1)

def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u


This was a bit of a surprise to me. A more common pattern would be to define is_unit as a structure with three fields, and then units as a dependent pair, an element and evidence that it was a unit.

I guess the current design has the (small?) advantage that we can put is_unit in Prop, rather than just show it's a subsingleton.

#### Johan Commelin (Sep 13 2019 at 05:10):

I guess the reasoning is: the type of units must record the inverse, not only its existence, and is_unit must be a Prop. Under those two conditions, the resulting definitions are quite reasonable....

#### Mario Carneiro (Sep 13 2019 at 05:36):

The only reasonable variation I can see is to make is_unit a type that records the inverse (and is a subsingleton). With that version you could factor it the other way around, but if is_unit is a prop then this approach is easier

#### Mario Carneiro (Sep 13 2019 at 05:38):

I believe is_unit came later, and it was needed for defining an ideal or something so it was necessary for it to be a prop

#### Yury G. Kudryashov (Sep 18 2019 at 22:36):

At the same time, e.g., is_iso records the inverse. If we need Prop, we can always use nonempty (is_unit x).

#### Mario Carneiro (Sep 19 2019 at 02:15):

I would argue that is_iso is not following the naming convention then, although maybe it's fine if the propositional version is not useful in category theory

#### Mario Carneiro (Sep 19 2019 at 02:18):

We should come up with a naming convention for these "witnesses in Type" for existential predicates, but I'm at a loss as to what it should be. unit_of? inverse?

Last updated: May 18 2021 at 08:14 UTC