iwilare

Stream: new members

[Andrea Laretto]

Hello!

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:

https://github.com/iwilare/mathlib4/tree/subcategory
https://github.com/iwilare/mathlib4/blob/subcategory/Mathlib/CategoryTheory/Subcategory.lean

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]

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

[Andrea Laretto]

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]

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]

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]

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

[Anne Baanen]

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]

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]

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]

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]

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]

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.