[Merged by Bors] - feat: add unitor functor for product of categories

[onriv]

left and right unitor functors for product of categories

---

The implementation is copying from the same file for the associator. I am not sure if the category "1" , i.e., Discrete Punit should take universe parameter or not, and if it should have some notation like U+1D7CF 𝟏 or something else.

[github-actions]

PR summary 9f3684242a

Import changes

No significant changes to the import graph

---

Declarations diff

+ leftInverseUnitor
+ leftUnitor
+ leftUnitorEquivalence
+ leftUnitor_isEquivalence
+ rightInverseUnitor
+ rightUnitor
+ rightUnitorEquivalence
+ rightUnitor_isEquivalence

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[erdOne]

Thanks for the contribution! If you think this PR is ready for review please add the "awaiting-review" label. While you're at it, adding the "t-category-theory" tag also helps the discoverability of the PR. Also see this page for more info.

[onriv]

@erdOne Thank you for the reply! Yeah I added the two tags and reading the doc now.

[joelriou]

As the file is named Associator.lean, could you move the new code to a new file Unitor.lean.

[onriv]

@joelriou Thank you for the suggestion! New code moved to a new file Unitor.lean.

[joelriou]

You may have to update the root file Mathlib.lean so that all files (including the new one) are imported.

[onriv]

@joelriou Thanks for the reminding! Mathlib.lean updated too. It's kind of weird that the ci pipline failed now though

[joelriou]

And similarly below:

Suggested change

	def leftUnitor : Discrete (PUnit: Type w) × C ⥤ C where
	def leftUnitor : Discrete (PUnit : Type w) × C ⥤ C where

[onriv]

Thanks! Codestyle change with space before column now

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style