Zulip Chat Archive
Stream: general
Topic: LNU and GAFT
Dean Young (Dec 31 2022 at 22:16):
I'm looking for some documentation on how Lean handles LNU (Tactics for choosing the Least Number of Universes) and GAFT (General Adjoint Functor Theorem).
Junyan Xu (Dec 31 2022 at 22:32):
The latter is apparently https://leanprover-community.github.io/mathlib_docs/category_theory/adjunction/adjoint_functor_theorems.html
I don't think there is a tactic for choosing the least number of universes in Lean; what's the purpose? mathlib declarations are generally universe polymorphic.
Yaël Dillies (Dec 31 2022 at 22:34):
A while back, @Mario Carneiro wrote some meta code that figures out the minimum universes that make a declaration typecheck.
Mario Carneiro (Dec 31 2022 at 22:35):
Last updated: Dec 20 2023 at 11:08 UTC