`{Funext} {G : Graph} {D : Diagram G} {Q1 Q2 : Type} (HQ1 : IsLimit D Q1) (HQ2 : IsLimit D Q2) : Q1 <~> Q2. Proof. srapply equiv_functor_limit. srapply (Build_diagram_equiv (diagram_idmap D)). Defined.
Require Import Basics. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cone. Require Import Diagrams.ConstantDiagram.