Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.8K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#cubicalagda

0 posts0 participants0 posts today
Cass Alexandru<p>Ok so the past few days a lot of criticism of indexed inductives in <a href="https://types.pl/tags/cubicalagda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>cubicalagda</span></a> <a href="https://types.pl/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda</span></a> has been going in and this is just my two cents from a user perspective but I defined (a datatype for lists indexed by the multisets of their elements)[<a href="http://partiallyapplied.eu/correct-bialgebraic-sorting/DistrLaw.html#1275" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">http://</span><span class="ellipsis">partiallyapplied.eu/correct-bi</span><span class="invisible">algebraic-sorting/DistrLaw.html#1275</span></a>] and successfully used it to define intrinsically correct sorting algorithms using bialgebraic semantics.</p>
Hexirp Prixeh<p><a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a><span> </span><a href="https://misskey.io/tags/HoTT" rel="nofollow noopener noreferrer" target="_blank">#HoTT</a><span> </span><a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a><span> </span><a href="https://misskey.io/tags/CubicalTypeTheory" rel="nofollow noopener noreferrer" target="_blank">#CubicalTypeTheory</a><span> </span><a href="https://misskey.io/tags/定理証明支援系" rel="nofollow noopener noreferrer" target="_blank">#定理証明支援系</a><span> </span><a href="https://misskey.io/tags/CubicalAgda" rel="nofollow noopener noreferrer" target="_blank">#CubicalAgda</a><span><br><br>RE: </span><a href="https://mathstodon.xyz/users/mortberg/statuses/111379610737862540" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/mortberg/statuses/111379610737862540</a></p>
SearchLive feeds
About