fact: Definition cone_precompose_inv `{D: Diagram G} {Q X} (H : IsLimit D Q) (C' : Cone X D) : X -> Q := @equiv_inv _ _ _ (islimit_unicone H X) C'.
imports: Basics Diagrams.Diagram Diagrams.Graph Diagrams.Cone Diagrams.ConstantDiagram