Commit 2021-04-06 01:49 13f7910b

feat(category_theory/limits/kan_extension): Right and Left Kan extensions of a functor (#6820) This PR adds the left and right Kan extensions of a functor, and constructs the associated adjunction. coauthored by @b-mehta A followup PR should prove that the adjunctions in this file are (co)reflective when \iota is fully faithful. The current PR proves certain objects are initial/terminal, which will be useful for this.