On Irrelevance vs Prop

[JacquesCarette]

@jespercockx hints in agda/agda#543 that we might be able to replace some uses of irrelevance with Prop. So I have two questions,

1. Is Prop likely to become standard enough to use in the standard library?
2. Would Prop be sufficient to get the 'equalities' wanted in a library like the categories one? [Some constructions on Natural Transformations need some categories to be equal in a proof-irrelevant way, which is currently achieved using irrelevance].
   I want to start the (incremental) process of moving categories into stdlib, and this is one of the blocking big-design decisions.

[gallais]

Some related discussion in #645:

• a use-case for Prop I find interesting
• @nad rightfully points out that some people may not want to use all of the agda features

I guess the second point doesn't apply quite as much to your project: the use of
Prop would be fairly circumscribed to that part of the library as opposed to
Data.Empty which is all encompassing.

[MatthewDaggitt]

1. Is Prop likely to become standard enough to use in the standard library?

As @gallais says above, I think that if they are kept to the category theory portion of the library then there is no problem in using them if they turn out to be a feature that drastically simplifies the code.

2. Would Prop be sufficient to get the 'equalities' wanted in a library like the categories one?

From my limited understanding, yes, but I'm sure there are people more qualified to answer that one.

[MatthewDaggitt]

Closing this as I think it's been answered.