`{Funext} (D : Diagram G) (X : Type) : DiagramMap D (diagram_const X) <~> Cocone D X. Proof. srapply equiv_adjointify. 1,2: intros [? w]; econstructor. 1,2: intros x y z z'; symmetry; revert x y z z'. 1,2: exact w. 1,2: intros[]. 1: srapply path_cocone. 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.