Q1 <~> Q2 := Build_Equiv _ _ _ isequiv_functor_colimit.
Require Import Basics Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.ConstantDiagram. Require Import Colimits.Coeq.