Lifting sheaves from the basis of a distributive lattice

[mzeuner]

This PR proves a "comparison lemma" for sheaves on distributive lattices: Given a presheaf on a basis of a distributive lattice taking values in an arbitrary category (with limits) and satisfying a sheaf property for bases, this can be extended to a sheaf on the whole lattice.

There seems to be quite a bit of overlap in the files Cubical.Categories.Presheaf.KanExtension and Cubical.Categories.Limits.RightKan the latter being a bit more general. Eventually these should be merged or the results upstreamed, but maybe that's something for a different PR?