{D : Diagram G} `(f : Q <~> Q') : IsLimit D Q' -> IsLimit D Q. Proof. intros HQ. srapply (Build_IsLimit (cone_precompose HQ f) _). apply cone_precompose_equiv_universality, HQ. Defined.
Require Import Basics. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cone. Require Import Diagrams.ConstantDiagram.