Add properties of ⌊_⌋

[gallais]

We do not have of the properties of ⌊_⌋ as far as I can tell.

E.g. ⌊ Dec.map′ t f d ⌋ is equal to ⌊ d ⌋.

[jamesmckinna]

For your example result:

⌊⌋-map′ : ∀ t f (a? : Dec A) → ⌊ map′ {B = B} t f a? ⌋ ≡ ⌊ a? ⌋
⌊⌋-map′ t f (true  because _) = refl
⌊⌋-map′ t f (false because _) = refl

or else

⌊⌋-map′ : ∀ t f (a? : Dec A) → ⌊ map′ {B = B} t f a? ⌋ ≡ ⌊ a? ⌋
⌊⌋-map′ t f a? rewrite isYes≗does (map′ t f a?) | isYes≗does a? = refl

using the existing Relation.Nullary.Decidable.isYes≗does (and in the first version, echoing its proof almost entirely).

A(nother) possible instance of the Fairbairn threshold not being met?

What else did you have in mind?

[JacquesCarette]

I think that, in Agda, the Fairbairn threshold is quite a complex affair: one should really be counting the (implicit) number of reductions and delta-expansions that are needed for the result to be trivial. I'd add these properties explicitly.

[jamesmckinna]

Agree it's not a straightforward question, apologies for suggesting it might be... but there has been quite a lot of recent invocation of the criterion in relation to such matters ...