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