I am not aware of anything inside Agda's standard library, but it provides almost what you need in the Function
module. You can do without ∈Wrap
. Let me propose a little syntactic sugar:
infix 4 _⟧
infixr 3 _─_⟶_
infix 2 _⟦_
_⟧ : ∀ {α} → (A : Set α) → A → A
_⟧ _ = id
_⟦_ : ∀ {α β} {A : Set α} → (a : A) → {B : A → Set β} → ((x : A) → B x) → B a
a ⟦ f = f a
_─_⟶_ : ∀ {α β γ} (A : Set α) → {B : A → Set β} → (f : (a : A) → B a) →
{C : {a : A} → (b : B a) → Set γ} → (∀ {a} → (b : B a) → C b) →
(a : A) → C (f a)
A ─ f ⟶ g = g ∘ f
Then you can write your proof as:
...
even-sqrt {suc (suc n)} (esuc e) = e ⟦
Even (n + suc (suc (n + n * suc (suc n))))
─ subst Even (+-comm n (suc (suc (n + n * suc (suc n))))) ⟶
...
─ remove-*2 n ⟶
Even (n * n)
─ even-sqrt2 {n} ⟶
Even n
─ esuc ⟶
Even (suc (suc n)) ⟧
The main benefits of this variant are:
- There is no wrapper type. You are just working with functions.
- The nesting is done the right way. With the approach presented in the question, you cannot refine a hole at the end with
_$⟨_⟩_
, so you always end up editing code outside the last hole.
It would be nice to have this functionality in the standard library and the way to do that currently is to open an issue or pull request on github. Can you do that?