Lemma is_functor_ColimFunctor_data : is_functor ColimFunctor_data. Proof. split. - intro a; simpl. apply pathsinv0, colim_endo_is_identity; intro u. unfold ColimFunctor_mor. now rewrite colimOfArrowsIn, (functor_id (dob D u)), id_left. - intros a b c fab fbc; simpl; unfold ColimFunctor_mor. apply pathsinv0. eapply pathscomp0; [now apply precompWithColimOfArrows|]. apply pathsinv0, colimArrowUnique; intro u. rewrite colimOfArrowsIn. rewrite (functor_comp (dob D u)). now apply pathsinv0, assoc. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.