Why is hProp a Record rather than a sigT?

[mikeshulman]

I know we discussed this a little bit ago, but I don't remember where or what the arguments were. It seems to me that making it a sigT would have the following advantages:

1. All the theorems about sigmas would apply to it directly, rather than via issig. We wouldn't have to prove two copies of some theorems, like path_equiv_biimp and path_equiv_biimp_rec in epi.v (which ought to be named something more descriptive also).
2. We wouldn't have to remember the names of special constructors and destructors like hp and hproptype; we could just use the ordinary pairing (_;_) and projections pr1 and pr2. The first time I encountered the constructor hp I was very confused.
3. It would be definitionally equal, rather than just equivalent, to @TypeO (truncation_modality -1), so we could apply any theorems about the latter to it directly.

The same applies to hSet and to TruncType (of which hProp and hSet ought to be special cases rather than their own definitions in any case).

[andrejbauer]

Most of these reasons apply to most records in the library, don't they?

[JasonGross]

Records with more than two fields would need to be nested sigma types; using nested projections is painful (e.g., replacing identity C x with x.2.2.2.1 for precategories), and defining named projections would lose the benefit of primitive projections.

We also can't make pr1 and pr2 coercions, and so we'd have to define extra functions to use as coercions. Because things like rewrite aren't up to delta, this might cause the occasional mismatch between a theorem using coercions and a theorem using pr1.

Personally, I prefer records for everything, because this enforces more modularity, and allows us to change the underlying representation, if we wish, without having to change every use of the type. But I'd be ok with replacing the two-field records that don't register either field as a coercion, with sigma types. (I'm not sure how I feel about replacing the ones involving coercions, but if they build without much trouble, I'd probably be fine with it.)

I'm not necessarily advocating the following, but want to propose the possibilities:

Regarding 2, we can make a scope for hProp and hSet, and bind (_;_) to the relevant constructors within that scope. Then, in many cases, Coq can pick up automatically which one we mean (the exception being when we're defining an hProp/hSet as, say, the return of a function or a top level definition, rather than to pass as an argument).

Regarding 2 and 3, we can make a coercion hProp >-> sigT. This should eliminate the need to remember the destructors, at the cost of introducing an extra function into some definitions, and apply <TypeO theorem> could probably be made to work in this manner.

[spitters]

The exists tactic works for records BTW.

We are currently not using Canonical Structures/ Type Classes a lot, so the
benefits are less clear.
Our statements look less nice than they could be, since we are using a
completely unbundled approach. E.g.

Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A) : Contr A.

Could be

Lemma contr_inhabited_hprop (A : hProp) (x : A) : Contr A.

It's easy to find more elaborate examples. Of course, this can be done with
sig too, but we'd lack the support for automation.

This was a choice at some point, but we may want to reconsider. Although,
I've tried to play with it a bit, but it is not entirely clear how to make
maximal use of this.

On Thu, Sep 18, 2014 at 8:27 AM, Andrej Bauer notifications@github.com
wrote:

These reasons apply to most records in the library, don't they?

—
Reply to this email directly or view it on GitHub
#514 (comment).

[mikeshulman]

I agree that records with 3+ fields are generally preferable to nested sigmas. But for 2-field records, especially those whose second field is an hprop, I'm not convinced. I'd like to try it, with coercions, and see whether we run into any trouble.

Another possibility, which I wouldn't like as much but I think would be preferable to the current situation, would be to define a general Subset record that is just a general sigma whose second component is an hprop. Then we could declare the first projection of Subset to be a coercion (which we wouldn't want to do for all sigmas), and define things like hProp using Subset. We could duplicate the relevant parts of types/Sigma.v in types/Subset.v.

The advantage of the unbundled approach is that sometimes we have a type and we know that it's an hprop, but it isn't given to us as an element of hProp. With the first projection of hProp declared as a coercion and the second as an instance, the unbundled version is applicable wherever the bundled one would be, but not conversely. Am I wrong?

[mikeshulman]

(Or maybe Subtype would be better since its first component is not necessarily a set.)

[spitters]

With the first projection of hProp declared as a coercion and the second
as an instance, the unbundled version is applicable wherever the bundled
one would be, but not conversely. Am I wrong?

We could try harder, but it is not so clear how to do it.
In fact, the unbundled approach is what we developed in our math-classes
library.
http://math-classes.org/
http://dx.doi.org/10.1017/S0960129511000119

The Program tactic was precisely developed to work nicely with subtypes.

On Thu, Sep 18, 2014 at 7:09 PM, Mike Shulman notifications@github.com
wrote:

I agree that records with 3+ fields are generally preferable to nested
sigmas. But for 2-field records, especially those whose second field is an
hprop, I'm not convinced. I'd like to try it, with coercions, and see
whether we run into any trouble.

Another possibility, which I wouldn't like as much but I think would be
preferable to the current situation, would be to define a general Subset
record that is just a general sigma whose second component is an hprop.
Then we could declare the first projection of Subset to be a coercion
(which we wouldn't want to do for all sigmas), and define things like
hProp using Subset. We could duplicate the relevant parts of types/Sigma.v
in types/Subset.v.

The advantage of the unbundled approach is that sometimes we have a type
and we know that it's an hprop, but it isn't given to us as an element of
hProp. With the first projection of hProp declared as a coercion and the
second as an instance, the unbundled version is applicable wherever the
bundled one would be, but not conversely. Am I wrong?

—
Reply to this email directly or view it on GitHub
#514 (comment).

[mikeshulman]

The discussion at #543 is very relevant to the argument against using sigmas in the presence of coercions. The confusion that I imagined, and @marcbezem experienced, shows very clearly, I think, that we don't want fields like hproptype (rather than some renaming of them) to be coercions. An occasional mismatch requiring an extra unfold before rewriting (which would happen after renaming the coercions whether or not the underlying record were a sigma) is, I think, a very acceptable price to pay for eliminating this confusion.

[Alizter]

@mikeshulman Is this issue resolved now?

[Alizter]

It should be noted that sigT is implemented itself as a record type with two fields. Therefore it stands to reason that Records and sigma types are equivalent in this case, performance wise. The only real difference being the coercions/subtyping.

So do we want to have coercions/subtyping or allow for various sigma type lemmas to work?

[JasonGross]

They are definitely not equivalent performance-wise if you work with named projections. If we want to be able to have named definitions for the protections of hProp (rather than notations), then we lose all of the benefit of primitive projections.

(There is another small cost: unification may be slightly slower to fail when trying to unify hProp against another sigma type.)

However, it may turn out that in practice these costs are negligible.

[mikeshulman]

Well, point #2 in the OP suggested that we shouldn't have special names for the projections of hProp. Why would we?

[Alizter]

Just to bump this issue, now that we have more control over how sigma types are defined, it may be useful to experiment with this again. I think there are some potential advantages to what Mike highlighted.