Definition constantFunctor (C:category) {D:category} (d:D) : [C,D]. Proof. unshelve refine (makeFunctor _ _ _ _). - exact (λ _, d). - intros c c' f; simpl. exact (identity d). - intros c; simpl. reflexivity. - abstract (simpl; intros a b c f g; apply pathsinv0, id_left) using _L_. Defined.
Require Import UniMath.MoreFoundations.Tactics.