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 (https://tdejong.com/phd-thesis.pdf) and on arXiv (https://arxiv.org/abs/2301.12405).

ANN: #Agda 2.6.3 is out today! 🐔🎉

Get yours here: https://hackage.haskell.org/package/Agda

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

I should write a VSCode plugin for #forester.

PSA: The #SciHub sci-hub.se domain was seized by the swedish domain registrar.

The current active mirrors are

https://sci-hub.ru

https://sci-hub.st

Alexandra recommended .ru

TorrentFreak has more information:

https://torrentfreak.com/domain-registry-takes-sci-hubs-se-domain-name-offline-230126/

A prior post for context:

https://social.coop/@jonny/109717676964759400

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.

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

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.

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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, the abstract, and a list of all upcoming talks.

All are welcome!

#HoTT @carloangiuli@twtr.plus @carloangiuli@birdsite.wilde.cloud @emilyriehl