You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Elisha Goldman (Oct 22 2025 at 17:17):Whenever I use Lean, my code always ends up swamped in bookkeeping because the compiler raises errors like Expected type X but received type (X, X).fst, even though my code in actual programming languages doesn't really have this issue. Are there bad habits I'm falling into unknowingly, or do other theorem provers make this easier?
Nathanael Arkor (Oct 22 2025 at 17:32):I imagine you will have more success asking this kind of question on https://leanprover.zulipchat.com/.
Nathan Corbyn (Oct 22 2025 at 18:00):In my experience it’s a very active Zulip and a very welcoming community
Ryan Wisnesky (Oct 22 2025 at 22:48):That's a peculiar error in any dependent type theory; one would expect X and (X,X).fst to be convertible in any context by the beta rule for products
James Deikun (Oct 22 2025 at 22:54):Lean may be like Rocq and hold off applying the conversion rule until explicitly asked.
Elisha Goldman (Oct 22 2025 at 23:35):I think James is probably right, those errors only occur when it needs to implicitly convert while doing something else, and writing by simp fixes them 99% of the time, it's just that rewriting so much code to fit by simp in is not ideal
Josselin Poiret (Oct 23 2025 at 09:44):James Deikun said:
Lean may be like Rocq and hold off applying the conversion rule until explicitly asked.
Rocq does not do what you describe: if two things are convertible (such as x and (x, y).fst), the kernel will always find that these are convertible. The typechecking and conversion algorithms are not interactive in Rocq (and that's the same in Lean).
Josselin Poiret (Oct 23 2025 at 09:46):one difference is that Lean's conversion is in general undecidable, so that the implemented algorithm may sometimes fail to see that two things are convertible, but I don't think a simple problem such as X ≡ (X, X).fst would fail
Mike Shulman (Oct 23 2025 at 21:44):However, one "gotcha" in Rocq is that not everything happens "up to convertibility", such as typeclass inference. If two types are convertible, it doesn't follow that a typeclass instance belonging to one of them will necessarily be found when searching based on the other. I don't know if Lean also has this issue.
Josselin Poiret (Oct 24 2025 at 09:05):same for tactics: lots of them will only be up to syntactic equality, not conversion. These are all part of the higher layers of Rocq that build terms for the kernel though, so you will never get a complaint from the kernel saying that two specific things are not convertible, only that some tactic or typeclass search failed.