It would be nice to prove that Kan Extensions involving the terminal category align with (co)limits

[JasonGross]

We've actually gone out of our way in agda-categories to make as many of these things hold judgementally. For 1 -> C vs C, that is hopeless, as they are fundamentally different even if equivalent (though there might be odd things when C is not inhabited). Certainly (1 -> C ᵒᵖ) should be the same as (1 -> C) ᵒᵖ, and it something that can be fixed if it's not. For Kan extension, it's possible we've erred, and we'd be glad to see a concrete bug report.

Originally posted by @JacquesCarette in https://github.com/agda/agda/issues/5255#issuecomment-790045655

As far as I can tell, you directly define left and right Kan extensions, but don't prove that this construction is equivalent to being adjoints to the functor that exhibits the functoriality of functor composition (p* in Global Kan Extensions in nLab). (In HoTT/HoTT in Coq, we define this here.) Observation 2.2 indicates that if C' is the terminal category, then Kan Extensions should align with (co)limits. The goal is to have a version of Kan extensions where you only need one proof of this alignment (either for left/colimit or for right/limit), which you can reuse in dualized form for the other side. (I have some partial work in Coq on realizing this alignment here, which I eventually shelved for lack of progress on Coq's version of https://github.com/agda/agda/issues/5255 (https://github.com/coq/coq/issues/5293#issuecomment-337550412) (together with Coq not having judgmental eta for records without any fields (https://github.com/coq/coq/issues/5291)).)

[JasonGross]

See also https://github.com/agda/agda-categories/issues/256