# Zulip Chat Archive

## Stream: general

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

#### Junyan Xu (Nov 20 2021 at 08:36):

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 ...

Last updated: Dec 20 2023 at 11:08 UTC