<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>