Can I block or hide people boosting some content I've already read? Maybe just show a line telling me somebody has boosted..

Trebor boosted

My PhD thesis, supervised by @MartinEscardo, on domain theory in constructive and predicative HoTT/UF is now publicly available!
It's both on my homepage ( and on arXiv (

Final decision. The domain thing is... too big. One iteration is too trivial, and the next cannot fit in my computer.

Trebor boosted

ANN: 2.6.3 is out today! 🐔🎉
Get yours here:

Here on types, I can make a longer post, rather than a tiny thread, about the headline changes:

⏩ A ton of performance improvements, which total to a ~30% improvement over in time spent for the standard library;

🧊 Erased Cubical Agda, which marks all marks all Cubical Agda definitions (primitives and imports from other --cubical modules) as @​0, quantity-0. The upshot is that you can reason about your programs using cubical machinery (funext!
HITs! univalence!), but nothing cubical "survives to runtime" — because unlike plain Cubical Agda, Erased Cubical can be compiled, using any of our backends (Haskell, JS) or agda2hs.

🇰 For a while during 2.6.3's development, --without-K also meant "generate support code for Cubical Agda". This was widely regarded as a bad move and made a lot of people very unhappy, so we rolled it back: Your --without-K code will no
longer suffer from cubical breakouts, and especially no longer enjoy surprise hcomps in error messages. The trade-off is that, if you want your modules to be usable from Cubical Agda (--cubical), you need to use the new
--cubical-compatible flag. Since --cubical-compatible does a ton extra (required!) internal work, modules using it will generally take longer to check, and generate larger interfaces files than, the same modules --without-K.

⚠️ Note that --cubical-compatible and --without-K should accept the exact same programs; This means you could develop against --without-K, then change to --cubical-compatible for release, for example. If you find something that one
accepts and the other rejects, please do file a bug report! On GitHub. Not on my DMs.

🪞 Reflection can now generate data types, as long as you pre-declare the names of the type and all the constructors, using the declareData and defineData primitives, together with the unquoteDecl data syntactic form. These even work for
inductive-recursive and inductive-inductive definitions!

🙏 A massive thanks to everyone who contributed to this release. Git tells me that, since the last tag, these lovely folks authored commits on the master branch:

Moisés Ackerman, Andrej Bauer, Jacques Carette, Evan Cavallo, Felix Cherubini, Jonathan Coates, Lucas Escot, Robert Estelle, Alexandre Esteves, Naïm Favier, Sean Gloumeau, Oleg Grenrus, Marcin Grzybowski, Matthias Hutzler, Tom Jack, Andre Knispel, Thomas Lamiaux, Shea Levy, Viktor Lin, Vladimir Lopatin, Sandy Maguire, James Martin, Orestis Melkonian, Fredrik Nordvall Forsberg, Andreas Nuyts, Kyle Raftogianis, Prabhakar Ragde, Christian Sattler, Peter Selinger, Artem Shinkarov, Mike Shulman, Alissa Tung, Andrea Vezzosi, Szumi Xie, Tesla Zhang, Fangyi Zhou; Favonia, lawcho, Maštarija, oskeri, person-with-a-username, Riccardo, tensorknower69, and thorimur.

Some of them are here on Fedi, but I don't want to bother them all with pings, so I won't.

🧑‍💻 Our tireless main developers (🤓❤️) also deserve a great big round of applause, not only for finishing the release, but for all they do for the language,
especially since most have real jobs, too!

Andreas Abel, Guillaume Allais, Nils Anders Danielsson, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Ulf Norell, and Andrés Sicard-Ramírez.

If you want to get involved, please reach out! We always welcome pull requests and issue reports, be them to Agda itself, the Emacs mode, both their documentations, the standard, cubical, and categories libraries. We promise nobody will get
bitten for submitting a pull request 🙂

I think I'll go for (an approximation of) a domain satisfying \(D = [D \to D]\). This should behave like a profinite set, and I can draw it iteratively.

Show thread

I need some concept in type theory that can generate a nice picture for book covers or that sort of thing. Any recommendations?

How do I justify eta-long normal forms to somebody coming from a math background?

Trebor boosted

PSA: The #SciHub domain was seized by the swedish domain registrar.

The current active mirrors are
Alexandra recommended .ru

TorrentFreak has more information:

A prior post for context:

Trebor boosted

"I hope this graffiti lowers housing cost$"
Seen in Bellingham Washington

Agda has explicitly cumulative universes, and with the --cumulative flag it becomes implicitly cumulative. Saying Agda is "non-cumulative" is straight up lying.

Trebor boosted

I enjoyed David Renshaw's 11-minute supercut of 2 hours of formalizing an IMO problem in Lean 4. Lots of things in the system and library that work, lots that could be improved!

A rack is an algebraic structure with two operations, satisfying
(a>b)>c = (a>c)>(b>c)
a<(b<c) = (a<b)<(a<c)
(a<b)>a = b = a<(b>a).
A quandle additionally satisfies a<a = a = a>a.

Note that every group gives rise to a quandle via conjugation. Define a>b = b^(-1)ab, and a<b = aba^(-1). Group conjugations satisfy exactly the quandle axioms, and no more. So quandles can be thought of as forgetting everything about a group except conjugations.

Quandles are used to compute knot invariants. The fundamental group of a knot (defined as the topological fundamental group of the knot's complement in R³) can be presented using only conjugations. So each knot has a fundamental quandle. Many knot invariants are actually the number of morphisms of the fundamental quandle to other quandles.

Trebor boosted

@ohad @pigworker Don't listen to the old folks, do treat contexts like DAG. Just because DAGs are awful syntactically (unlike snoc lists) doesn't mean they're not closer to a good representation.

But I think Conor is going one step further: I would phrase it as thinking of contexts co-algebraically. If you have a variable in scope, you can always "ask the context" what type it has, and it is guaranteed to answer (with a well-formed type). That's basically the only question a context guarantees it will answer.

Trebor boosted

Stray thought: wanting all one's proofs to live in `Prop` is premature optimization.

The nice thing about `Prop` is that it's contractible - so you can erase terms from it, as it they have no computational content left in them. And the backwards thinking begins: for efficiency, we don't want our nice computations to be polluted by proofs / slowed down by computing useless proofs, SOOOO let's put them all in `Prop`!

Err, no. Many proofs are rather valuable beyond their mere existence.

Putting proofs "where they want to live" (that could be Set, Cat, Bicat, DblCat, etc), AND THEN deciding to throw some away is a much better idea than a priori throwing them all away.

Trebor boosted
Trebor boosted

I think it's important to follow a few people where you never have any idea what the fuck they're talking about but it seems interesting

Trebor boosted
Trebor boosted

This week the #HoTTEST seminar presents:

Johan Commelin

The Liquid Tensor Experiment

The talk is 11:30am-12:30pm EST (UTC-5) on Thursday, January 26 and will be followed by discussion. See for the Zoom link, the abstract, and a list of all upcoming talks.

All are welcome!

#HoTT @emilyriehl

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.