Zulip Chat Archive

Stream: maths

Topic: units and is_unit


view this post on Zulip 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.

view this post on Zulip 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....

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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