[Merged by Bors] - feat(category_theory): full_of_surjective

[TwoFX]

---

[urkud]

Why do you add two definitionally equal definitions? Also, I think that the new definition(s) should be mentioned in the module docstring.

More general question (definitely not for this PR): should we use a Type*-valued full, or a Prop-valued typeclass saying that map is surjective, then rely on lemmas instead of definitional equalities? Or sometimes you have different choices of preimage and one of them is better than others? In any case, this design choice should be explained in the module docstring. BTW, the link category_theory.equivalence in the module docstring is broken: it points to a definition, not a theorem.

[TwoFX]

@urkud I think that both (syntactic) statements are interesting on their own and before trying to prove the second one I didn't know that they are definitionally equal, so I added both. I can remove one of them if you want, but I think that it is plausible that someone needs one and doesn't immediately notice that it is definitionally equal to the other when looking for it.

Regarding the fact that full F is data: I think that this is mostly due to history, since the category_theory library used to have more data-carrying typeclasses like this than today (see for example #3995). There hasn't really been a need to change it so far, so I think it's fine to keep it like it is until someone feels that it should be refactored.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests