functor_colimit (diagram_equiv_inv m) HQ2 HQ1 o functor_colimit m HQ1 HQ2 == idmap. Proof. apply ap10. srapply (equiv_inj (cocone_postcompose HQ1) _). 1: apply HQ1. etransitivity. 2:symmetry; apply cocone_postcompose_identity. etransitivity. 1: apply cocone_postcompose_comp. rewrite eisretr, cocone_precompose_postcompose, eisretr. rewrite cocone_precompose_comp, diagram_inv_is_retraction. apply cocone_precompose_identity. Defined.
Require Import Basics Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.ConstantDiagram. Require Import Colimits.Coeq.