`{Funext} (X : Type) (D : Diagram G) : DiagramMap (diagram_const X) D <~> Cone X D. Proof. srapply equiv_adjointify. 1,2: intros [? w]; econstructor. 1,2: exact w. 1,2: intros[]. 1: srapply path_cone. 3: srapply path_DiagramMap. 1,3: reflexivity. all: cbn; intros; hott_simpl. Defined.
Require Import Basics. Require Import Cone. Require Import Cocone. Require Import Diagram. Require Import Graph.