Equivalence (or otherwise) of all the various definitions of proof-irrelevance; streamlining them

[jamesmckinna]

Consider:

• Relation.Binary.PropositionalEquality:

isPropositional : Set a → Set a
isPropositional A = (a b : A) → a ≡ b

• Relation.Nullary:

Irrelevant : ∀ {p} → Set p → Set p
Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂

• Relation.Unary:

Irrelevant : Pred A ℓ → Set _
Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b

• Relation.Binary.Definitions:

Irrelevant : REL A B ℓ → Set _
Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b

(these all fall under #2091 with the exception of the top one, which is defined but never used anywhere; nevertheless they are all 'propositional' accounts of irrelevance; UPDATED see #2259 )
and the type-theoretic/definitional account of irrelevance given by using .(_) as a syntactic marker on types:

• Data.Irrelevant
• Data.Empty.Irrelevant, which is built on top of it, likewise Data.Refinement
• the definition and use of recompute functions in Relation.Nullary.Decidable (cf. Inconsistencies between Relation.Binary.Definitions and Relation.Unary and Relation.Nullary #2091 again), which Enhancement to Relation.Nullary.Reflects etc. #2149 would seek to push down to Relation.Nullary.Reflects, along with a definition of Recomputable as a property of types. See also ⊥ is Recomputable #2199

Issue: how to reconcile all these various things in a straightforward and intelligible way?
And suitably redefine/deprecate the redundant ones...

[MatthewDaggitt]

isPropositional should be deprecated for starters....