units and is_unit

Stream: maths

[Scott Morrison]

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]

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]

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]

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]

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]

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]

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?