[Agda] unfolding just a single definition in the context of a goal

[Marcus Christian Lehmann]

Dear James,

Yes, that was helpful. Thank you for the clarification!

Introducing an additional record for these abbreviations (as in the 
standard library in Algrebra.Definitions [1]) feels to be against their 
purpose of being "lightweight" to use. Even when in control of the 
definitions. But it is a valid compromise, of course.

> If it's a variable (like in your example), you can create an alias of 
> it using `let`
> ...
> There's not really any way to automate this, but at least the type you 
> write down will be checked.

I am preferring this technique. Thank you for hinting towards it.

It seems to be even possible to use the very same name, e.g. for the 
purpose of inhibiting an outer-scope-parameter-renaming at all costs 
(which might be the favored way when other things in the same scope 
already depend on that parameter).

   sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X → 
wconstant-≡-endomaps X
   sets-have-wconstant-≡-endomaps' X p =
     let p : (x y : X) → is-subsingleton (x ≡ y)
         p = p
     in {!!}

gives an expanded `is-set`

   Goal: wconstant-≡-endomaps X
————————————————————————————————————————————————————————————
   p      : (x y : X) → is-subsingleton (x ≡ y)
   p      = p₁
   p = p₁ : is-set X   (not in scope)
   X      : Type ℓ

and the type annotation _∋_ that you suggested, with

sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X → 
wconstant-≡-endomaps X
   sets-have-wconstant-≡-endomaps' X p =
     let p : (x y : X) → is-subsingleton (x ≡ y)
         p = p
     in ((x y : X) → wconstant-endomap (x ≡ y)) ∋
        {!!}

givesan "expanded" `wconstant-≡-endomaps`

   Goal: (x y : X) → wconstant-endomap (x ≡ y)
————————————————————————————————————————————————————————————
   p      : (x y : X) → is-subsingleton (x ≡ y)
   p      = p₁
   p = p₁ : is-set X   (not in scope)
   X      : Type ℓ

When there is some name-clashing in a copied, too-complicated 
definition, it seems possible to put a lambda in there which mitigates 
the manual name translation a bit. E.g.

   sets-have-wconstant-≡-endomaps' : (Y : Type ℓ) → is-set Y → 
wconstant-≡-endomaps Y
   sets-have-wconstant-≡-endomaps' Y x =
     let x : (λ X → (x y : X) → is-subsingleton (x ≡ y)) Y
         x = x
     in (λ X → ((x y : X) → wconstant-endomap (x ≡ y))) Y ∋
        {!!}

gives an expanded and correctly renamed variant

   Goal: (x₂ y : Y) → wconstant-endomap (x₂ ≡ y)
————————————————————————————————————————————————————————————
   x      : (x₂ y : Y) → is-subsingleton (x₂ ≡ y)
   x      = x₁
   x = x₁ : is-set Y   (not in scope)
   Y      : Type ℓ

which looks managable enough to continue reasoning and might even be 
visually improved with an additional `syntax` for it.

kind regards,
Christian

[1] https://agda.github.io/agda-stdlib/Algebra.Definitions.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200713/2e668af7/attachment.html>