Transfer lax functor by adjunctions: Rewrite by defeq yie...

Stream: general

[Junyan Xu]

Last night I was able to prove the comp_id and id_comp compatibility conditions for the transferred lax functor, but it took one more night for me to figure out the associative compatibility and code it: when you expand the condition you get a composition of eight morphisms at each side of the identity, and there seems to be a lot of choices where to apply naturality, but it turns out applying them “maximally” is enough. I haven’t seen a proof before or even a reference for this transfer theorem, so I am glad that my intuition worked out right. Does anyone know a more conceptual proof?

The technical issue at the top of this thread about inability to rewrite no longer bothers me since last night, though dsimp only wasn’t actually useful because we can’t specify an argument so it ends up rewriting too much. And I didn’t end up using change; rewriting by right triangle first indeed worked well.

Now the task is to make the proofs faster and shorter; currently the three proofs take 5.5s, 6.5s and 16s on my machine.

And also to provide a simplified version in the case where map_id and map_comp are isomorphisms (pseudofunctor), where we can shave off an op (I think I don't need to repeat the proofs here); maybe I could also do the nLab version, as the proofs will be similar and won't add much effort.

This has been an unexpectedly long digression:
try to prove adjunction between overcategories Top/Y and PresheafedSpace/Y -> need the map_comp natural isomorphism for presheaf pullback -> try to define it in a canonical way -> find adjunction/mates that suites my need -> try to prove pseudofunctor compatibility conditions -> try to do it in "appropriate" generality of lax functors (but falls short of defining 2-categories ...), that's how I get here. And I'm not even sure the first goal (the adjunction) is necessary for the main project (existence of limits in PresheafedSpace and eventually in LocallyRingedSpace)! I should really get back to that ...