open import Cat.Prelude

module Cat.Diagram.End where

Ends🔗

Let $F : \ca{C}\op \times \ca{C} \to \ca{D}$ be a functor, which (by the general yoga of [bifunctors])