Zulip Chat Archive

Stream: new members

Topic: iwilare

Andrea Laretto (Oct 03 2023 at 12:19):


I'm Andrea, I'm a PhD student at Tallinn University of Technology. I'm quite experienced in Agda and type theory, I'm looking forward to try and experiment with Lean a bit, especially in the CategoryTheory section and maybe make some contributions!

I would like at some point to make some PRs about coends, categorical logic, and fibrations. For now I only have a small contribution ready where I just give a definition of Subcategories, which I couldn't find in the library... currently have it at this fork:


I might have at some point some questions on the best practices in Lean, coming from Agda... (like, is there such a thing as proper holes in Lean 4? Or am I doomed to just use by sorry everywhere just to get the type of a hole?)

Nice to meet you people! :big_smile:

Eric Wieser (Oct 03 2023 at 12:33):

I assume you're aware of docs#FullSubcategory, but it's not what you want?

Andrea Laretto (Oct 03 2023 at 12:37):

Yes, I saw that file, but no, I'm precisely trying to relax the Fullness requirement and just have something around the lines of https://ncatlab.org/nlab/show/subcategory

Anne Baanen (Oct 03 2023 at 13:08):

Welcome! If you'd like to make PRs, the best is to directly work on the main leanprover-community/mathlib4 repository. I can give you permission to do so on Github. Just to confirm: iwilare is your own username?

Andrea Laretto said:

is there such a thing as proper holes in Lean 4? Or am I doomed to just use by sorry everywhere just to get the type of a hole?

Yes! First of all sorry is also a term that means exactly the same as the tactic call by sorry, saving you a few characters :) More like Agda holes are _ and ?some_name, either Lean will figure these out through unification, or leave as a hole with an error.

Andrea Laretto (Oct 03 2023 at 13:30):

Yes, iwilare is my username, thank you!

I see, that's pretty useful; I have another small question: another thing that I miss a lot from Agda is not being able to inspect the WHNF of terms; I know of simp_all and reduce, but is there any way to simplify everything in the context? Full automatic unfolding of definitions would also be enough... especially for Hom, since I'm working within CategoryTheory, using unfold at seems to lead to too many unfoldings required, and I'm not sure that making everything as @[simp] is the best option.

Anne Baanen (Oct 03 2023 at 13:48):

Invite sent! https://github.com/leanprover-community/mathlib4/invitations

Anne Baanen (Oct 03 2023 at 13:52):

About unfolding: this is something I had to unlearn coming from Agda. Unfolding in Lean is supposed to be much more of an explicit decision than something that happens automatically, and if the library is correctly designed you should almost never have to unfold things. I'm not so familiar with the category theory library but the general idea is indeed that you mark enough things as @[simp] that you never have to use the unfold tactic.

Andrea Laretto (Oct 03 2023 at 14:05):

Thank you! I see, I think it's somewhat of a reasonable decision in order to avoid the "too simplified" problem... so I guess there's no way around by simp_all to check the simplified goal types and then switch back to term mode to actually fill in the proof? I was hoping there would be some global flag that could be set to fully reduce stuff (or at least some integration with the vscode extension)

Junyan Xu (Oct 03 2023 at 19:13):

We should probably have docs#CategoryTheory.Subgroupoid extend Subcategory when the latter is in mathlib ... Oh, I guess not, since a subgroupoid can be empty ...

Joël Riou (Oct 04 2023 at 14:51):

I would think that the definition of Subcategory could be slightly closer to the current mathlib definitions in CategoryTheory.FullSubcategory. If we have a category D, then the data for a subcategory of D could be that of a map F : C → D and a condition ∀ (X Y : C), Set (F X ⟶ F Y) which satisfies the compatibilities with identities and composition. Then, a suitable type synonym for C can be equipped with a category structure similarly as InducedCategory.category is defined.

Eric Wieser (Oct 04 2023 at 15:46):

I would think → Prop is more natural than Set there, but I guess your approach is more similar to things like Submonoid`

Joël Riou (Oct 04 2023 at 16:20):

I do not see the difference between ∀ (X Y : C), Set (F X ⟶ F Y) and ∀ (X Y : C), (F X ⟶ F Y) → Prop. What I suggest here is to allow any C which maps to D rather than only subtypes of D, similarly as full subcategories are defined in mathlib.

Last updated: Dec 20 2023 at 11:08 UTC