{D1 D2 : Diagram G} (m : D1 ~d~ D2) {Q : Type} : IsLimit D1 Q -> IsLimit D2 Q. Proof. intros HQ. srapply (Build_IsLimit (cone_postcompose m HQ) _). apply cone_postcompose_equiv_universality, HQ. Defined.
Require Import Basics. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cone. Require Import Diagrams.ConstantDiagram.