Shorter: Every u:∀M.Mi->Mj with ∀v:A->B.∀a∈Ai:uvia=vjua is just some {1,...,j}->{1,...,i}.
Note that Mi is just {1,...,i}->M, so in both our examples the map is backwards because we change domains.
Shorter: Every u:∀M.Mi->Mj with ∀v:A->B.∀a∈Ai:uvia=vjua is just some {1,...,j}->{1,...,i}.
Note that Mi is just {1,...,i}->M, so in both our examples the map is backwards because we change domains.