<p><span class="h-card" translate="no"><a href="https://types.pl/@jeremysiek" class="u-url mention">@<span>jeremysiek</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@rg9119" class="u-url mention">@<span>rg9119</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@wilbowma" class="u-url mention">@<span>wilbowma</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@sliminality" class="u-url mention">@<span>sliminality</span></a></span> yes, although you can also use it if you really want a cast (Robby and I wrote a STOP paper about that once).</p>