Topic: units and is_unit
Scott Morrison (Sep 12 2019 at 22:17):
Are we happy with the design of
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
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):
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.
Last updated: May 18 2021 at 08:14 UTC