Commit 2024-07-06 10:06 a347c63b

refactor(Bicategory/Functor): refactor prelaxfunctors (#14098) This PR suggests a refactor (and renaming) of prelax functors. This is to provide more reusability of code between oplax functors, pseudofunctors (and soon) lax functors. This is done in the following way:

• A new file is created called Bicategory.Functor.Prelax.
• What (before this suggested refactor) was called PrelaxFunctor, is renamed to LaxPrefunctor. Recall that this is a prefunctor that is also equipped with a map map₂ on 2-morphisms.
• A new structure is added, taking over the name PrelaxFunctor, which additionally requires that the associated prefunctors between hom types are functors. In other words, map₂ should respect identities and compositions.
• Both Pseudofunctor and OplaxFunctor are updated to extend the new notion of PrelaxFunctor. Finally: Coercions have also been removed between these various structures. This is to prevent the following behaviour in the current library: given a pseudofunctor F the infoview will print F.map as (↑F.toPrelaxfunctor).map which makes long expressions unecessarily hard to read. The change is just like how Functor does not have a coercion to PreFunctor. This refactor will allow us to define mapFunctor and map₂Iso on the level of PrelaxFunctors, which allows it to be reused for both Pseudofunctors and OplaxFunctors instead of having to be defined separately. A new constructors on this level has also been added, PrelaxFunctor.mkOfHomFunctors, that constructs a PrelaxFunctor given a map on types and functors between the corresponding hom types. This could for example be used to construct the pseudofunctor in the bicategorical yoneda lemma, by using the collection of functors precomposing (see Bicategory.Basic). The file CategoryTheory/WithTerminal has been edited just to fix the proof after these new changes.