Right Kan extension with an application to presheaves on DistLattices

[mzeuner]

This PR contains the right Kan-extension of a presheaf on a subset of a distributive lattice (seen as a sub-poset-category) to a presheaf on the whole lattice.

[mortberg]

Very nice!

I can't help but wonder if one could make this even more abstract by using https://github.com/agda/cubical/blob/master/Cubical/Categories/Presheaf/KanExtension.agda#L196 ? Maybe that definition unfolds to what you did here? It's nice that what you did here is much shorter though, but it could be that proving the sheaf property will be easier with a more abstract construction (for example if one wants to appeal to general abstract results like right adjoint preserving limits or commutation of limits...).

[mzeuner]

We're more general here since we consider presheaves in any category with limits, but then things get much easier since
we only consider inclusions of poset-categories...

Maybe it's worth doing the most general case à la MacLane:
If 𝑀 is small and 𝐴 is complete, then any functor 𝑇:𝑀→𝐴 has a right Kan extension along any 𝐾:𝑀→𝐶.

[mortberg]

We're more general here since we consider presheaves in any category with limits, but then things get much easier since we only consider inclusions of poset-categories...

Maybe it's worth doing the most general case à la MacLane: If 𝑀 is small and 𝐴 is complete, then any functor 𝑇:𝑀→𝐴 has a right Kan extension along any 𝐾:𝑀→𝐶.

Oh right, I see. I formalized the more general thing in UniMath some years ago: https://unimath.github.io/doc/UniMath/4dd5c17/UniMath.CategoryTheory.RightKanExtension.html#RightKanExtension_from_limits

As you can see it was somewhat longish, but I was able to follow MacLane X.3 (p. 233) very closely.

[mzeuner]

Ok, I managed to make the DistLattice case a special application of the general MacLane case. The proof should be pretty much the same.

[mzeuner]

left some TODOs for @mortberg