!4#3987 Topology.Gluing

Stream: PR reviews

[Damiano Testa]

This is essentially my first contact with category theory in Lean: I went through the file as best I could. If anyone is willing to review and maybe even give comments, I would be very grateful!

[Ruben Van de Velde]

Thanks!

[Damiano Testa]

I've been meaning for a while to do some category theory in mathlib and this seemed like an approachable entry point!