Agda-stdlib: Where to put a rather convenient function?

[JacquesCarette]

  refl₁ : {f : A → B} (x : A) → f x ≡ f x
  refl₁ _ = P.refl

A lot of proofs of simple things can infer f easily, and (λ _ → refl) gets tiresome.

[JacquesCarette]

(sorry about the initial blank issue, I hit 'enter' prematurely)

[gallais]

I have been thinking about this for a bit and I am reminded of the congruence
in Idris' standard library which takes its function argument implicitly. I am
tempted to propose this design (to be generalised to all the cong and subst):

open import Level
open import Function.Base
open import Relation.Binary.PropositionalEquality

variable
  a b : Level
  A : Set a
  B : Set b

-- i for implicit
icong : ∀ {f : A → B} {x y} → x ≡ y → f x ≡ f y
icong = cong _

-- ′ for simplified à la ∘′?
icong′ : ∀ {f : A → B} x → f x ≡ f x
icong′ {f = f} x = cong f refl

If we want we can also play the game in the other direction by introducing:

-- e for explicit
pattern erefl x = refl {x = x}

[JacquesCarette]

icong and icong′ would definitely work too. I would tend to create it at a low level (maybe even define these straight in Relation.Binary.PropositionalEquality.Base). The other-direction game is likely worthwhile for those cases where being explicit does clarify (at least for the reader).

I won't opine on subst variants -- I avoid subst like the plague, so as a non-user, I shouldn't have much of a say on it!

[MatthewDaggitt]

The proposed icong (as long as we use \prime and not '!) looks good to me.

I am tempted to propose this design (to be generalised to all the cong and subst):

I've _never_ come across a scenario where the function argument for subst can be inferred? Maybe I'm using it wrong!

[gallais]

I don't know if it happens often but see e.g.

open import Relation.Binary.PropositionalEquality.Core

transport : ∀ {A B : Set} → A ≡ B → A → B
transport = subst _

(we should by the way have something like transport or coerce or whatever
we may want to call it).

[JacquesCarette]

I've got a PR for Relation.Binary.PropositionalEquality open, I could add that at the same time. I prefer transport personally, but I would implement coerce if I'm in the minority 😄

[ajrouvoet]

We should by the way have something like transport or coerce or whatever
we may want to call it

I've been using a typeclass Respects parameterized by an equivalence on a type A and a predicate on A a lot. It has a single field coe. When the standard library is ready to use instances more this might be a nice generic utility.

[MatthewDaggitt]

Closed in #1224