<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p><tt>Dear James,
      </tt></p>
    <tt>
    </tt><tt>Yes, that was helpful. Thank you for the clarification!
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>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.
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt>
    <blockquote type="cite" style="color: #000000;"><tt>If it's a
        variable (like in your example), you can create an alias of it
        using `let`
      </tt><tt><br>
      </tt><tt>...
      </tt><tt><br>
      </tt><tt>There's not really any way to automate this, but at least
        the type you write down will be checked.
      </tt><tt><br>
      </tt></blockquote>
    <tt>
    </tt><tt><br>
    </tt><tt>I am preferring this technique. Thank you for hinting
      towards it.
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>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).
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>  sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X
      → wconstant-≡-endomaps X
    </tt><tt><br>
    </tt><tt>  sets-have-wconstant-≡-endomaps' X p =
    </tt><tt><br>
    </tt><tt>    let p : (x y : X) → is-subsingleton (x ≡ y)
    </tt><tt><br>
    </tt><tt>        p = p
    </tt><tt><br>
    </tt><tt>    in {!!}
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>gives an expanded `is-set`
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>  Goal: wconstant-≡-endomaps X
    </tt><tt><br>
    </tt><tt>————————————————————————————————————————————————————————————
    </tt><tt><br>
    </tt><tt>  p      : (x y : X) → is-subsingleton (x ≡ y)
    </tt><tt><br>
    </tt><tt>  p      = p₁
    </tt><tt><br>
    </tt><tt>  p = p₁ : is-set X   (not in scope)
    </tt><tt><br>
    </tt><tt>  X      : Type ℓ
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>and the type annotation _∋_ that you suggested, with
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X →
      wconstant-≡-endomaps X
    </tt><tt><br>
    </tt><tt>  sets-have-wconstant-≡-endomaps' X p =
    </tt><tt><br>
    </tt><tt>    let p : (x y : X) → is-subsingleton (x ≡ y)
    </tt><tt><br>
    </tt><tt>        p = p
    </tt><tt><br>
    </tt><tt>    in ((x y : X) → wconstant-endomap (x ≡ y)) ∋
    </tt><tt><br>
    </tt><tt>       {!!}
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>givesan "expanded" `wconstant-≡-endomaps`
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>  Goal: (x y : X) → wconstant-endomap (x ≡ y)
    </tt><tt><br>
    </tt><tt> 
      ————————————————————————————————————————————————————————————
    </tt><tt><br>
    </tt><tt>  p      : (x y : X) → is-subsingleton (x ≡ y)
    </tt><tt><br>
    </tt><tt>  p      = p₁
    </tt><tt><br>
    </tt><tt>  p = p₁ : is-set X   (not in scope)
    </tt><tt><br>
    </tt><tt>  X      : Type ℓ
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>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.
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>  sets-have-wconstant-≡-endomaps' : (Y : Type ℓ) → is-set Y
      → wconstant-≡-endomaps Y
    </tt><tt><br>
    </tt><tt>  sets-have-wconstant-≡-endomaps' Y x =
    </tt><tt><br>
    </tt><tt>    let x : (λ X → (x y : X) → is-subsingleton (x ≡ y)) Y
    </tt><tt><br>
    </tt><tt>        x = x
    </tt><tt><br>
    </tt><tt>    in (λ X → ((x y : X) → wconstant-endomap (x ≡ y))) Y ∋
    </tt><tt><br>
    </tt><tt>       {!!}
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>gives an expanded and correctly renamed variant
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>  Goal: (x₂ y : Y) → wconstant-endomap (x₂ ≡ y)
    </tt><tt><br>
    </tt><tt> 
      ————————————————————————————————————————————————————————————
    </tt><tt><br>
    </tt><tt>  x      : (x₂ y : Y) → is-subsingleton (x₂ ≡ y)
    </tt><tt><br>
    </tt><tt>  x      = x₁
    </tt><tt><br>
    </tt><tt>  x = x₁ : is-set Y   (not in scope)
    </tt><tt><br>
    </tt><tt>  Y      : Type ℓ
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>which looks managable enough to continue reasoning and
      might even be visually improved with an additional `syntax` for
      it.
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>kind regards,
    </tt><tt><br>
    </tt><tt>Christian
    </tt><tt><br>
    </tt><tt>
    </tt><tt><br>
    </tt><tt>[1] </tt><tt><a class="moz-txt-link-freetext"
        href="https://agda.github.io/agda-stdlib/Algebra.Definitions.html">https://agda.github.io/agda-stdlib/Algebra.Definitions.html</a></tt>
  </body>
</html>