feat(category_theory/groupoid/subgroupoid): subgroupoids and basic properties (#16742)
Add a definition of (bundled) subgroupoid and prove some of their basic properties.
Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
Co-authored-by: bottine <bottine@users.noreply.github.com>