Put notations in scope or make them local

[benediktahrens]

as suggested by Anders

[mortberg]

I had some trouble when working on presheaf categories because

https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/OtherDefs/CwF_Pitts.v

and

https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/ALV1/TypeCat.v

have some overlapping notations. There might be more notations that overlap which I didn't encounter. I think one can get coqc to print these as warnings to make them easier to detect (I know Dan did some changes to the UniMath Makefile to make it print certain warnings).