feat: port CategoryTheory.Bicategory.Free (#2482)

- [x] depends on: #2301 


Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Pol_tta <pol_tta@outlook.jp>
Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: MonadMaverick <MonadMaverick@pm.me>
Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
Co-authored-by: Matthew Robert Ballard <matt@mrb.email>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Pol_tta <MonadMaverick@pm.me>
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Author: 15 people

Mathlib.lean

@@ -472,6 +472,7 @@ import Mathlib.CategoryTheory.Arrow
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Basic
 import Mathlib.CategoryTheory.Bicategory.End
+import Mathlib.CategoryTheory.Bicategory.Free
 import Mathlib.CategoryTheory.Bicategory.Functor
 import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
 import Mathlib.CategoryTheory.Bicategory.Strict