Q1 <~> Q2 := Build_Equiv _ _ _ isequiv_functor_limit.
Require Import Basics. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cone. Require Import Diagrams.ConstantDiagram.