Show newer

@MartinEscardo
I had a question about univalent mathematics and I was told you'd be the one to ask. I hope you don't mind

Reading the HoTT book I noticed that they defined universes to be cumulative. This surprised me because in theorem provers such as Lean and allegedly Agda (I was told), this is not the case. In the book itself they mention a downside of having cumulative universes being that a term no longer has a unique type, but they don't mention any advantages of constructing them this way.

Therefore, my question is: what is the advantage of having cumulative type universes?

Ayhon boosted

** Speaker announcement ** Catch this talk at RustWeek 2025!

Speakers: David Barsky & Lukas Wirth
Title: Salsa in Rust-Analyzer

Info & tickets: rustweek.org/talks/salsa/

See you in Utrecht 13-17 May, 2025!

#rustweek #rustlang

Ayhon boosted

When Signal was designed, our threat model was protecting the communications of civil society, journalists, just regular citizens ...

The threat model of military operations & sharing your hate of Europeans was not what Signal was designed for. Ephemeral messages and cryptographic deniability are not fit for communications that require accountability.
But I appreciate their effort to make government more efficient by adding journalists to the chat instead of requiring to go through FOIA.

Ayhon boosted

Being confused about which account belongs to which person is known to security professionals as a state management problem.

I'll see myself out

Ayhon boosted

Which academic field has the best puns in paper titles? Examples welcome!

Ayhon boosted

I've now published my blog post, "I want a good parallel computer." raphlinus.github.io/gpu/2025/0 . Thanks much to all the feedback on the draft, I'd like to think I've clarified some things that might have been confusing.

Ayhon boosted

There are just a few days left now to register for the Midlands Graduate School (MGS) in Sheffield, 7-11 April 2025. Eight fantastic courses on category theory, type theory, coalgebra, semantics and more.

Registration closes on Monday 24th March.

tinyurl.com/MGS-2025

Ayhon boosted

The first production ready version of The Rocq Prover 9.0 has been released today, see rocq-prover.org/releases/9.0.0 on our new official website! In the coming weeks, we'll migrate the Discourse, Zulip and Github organizations, please bear with us and don't hesitate to report broken links! Packages for opam and nix will be coming soon.

Ayhon boosted
Ayhon boosted

Here is a followup to my previous "consolidate #Bevy microblogging" post, which includes our final decision:
github.com/bevyengine/bevy/dis

Ayhon boosted
Ayhon boosted

was trying to figure out how to implement some algebraic structures based on what i've been learning in my course on automated proof verifiers and anyway that's why i googled "coq rings" your honour

Ayhon boosted

36th European Summer School in Logic, Language and Information
2025.esslli.eu/

Registration is now open for students!

Boosts are appreciated.

#logic #computerscience

Ayhon boosted

Dear American friends, I know for a fact that many of you were as horrified as I was over the shameless display BLOATUS put on in the Oval Office yesterday.
I decided this morning that rather than seethe about it, I'd do something meaningful with my anger.
Below is the URL of Ukraine's official fundraising page. Maybe you could chip in a small amount, and/or give this a boost to spread the word? Thanks, and remember, there's still many more of us than of them!

u24.gov.ua/

Ayhon boosted
Ayhon boosted

Please boost and spread the word.
European alternatives for popular services from the USA. This page is far from perfect or complete but just an illustration that there are alternatives.
european-alternatives.eu/alter

This is also an interesting page with alternatives,
privacyguides.org/en/tools/

#EU #digitalservices #ICT #IT

Ayhon boosted

The second part of Grant Sanderson's video interview with myself on the cosmic distance ladder is now out: youtube.com/watch?v=hFMaT9oRbs

I wrote a blog post with additional commentary and corrections on both videos at terrytao.wordpress.com/2025/02

Ayhon boosted
Ayhon boosted
Ayhon boosted

Due to rising costs, I'll be adjusting the prices of my game assets. This helps maintain quality and allows me to continue creating content. There'll be a 10% price increase, making the new price... well, still $0 I guess. Thank you for understanding.

www.gameassets.com

Show older
Qoto Mastodon

QOTO: Question Others to Teach Ourselves
An inclusive, Academic Freedom, instance
All cultures welcome.
Hate speech and harassment strictly forbidden.