(D : Diagram G) : DiagramMap D D := Build_DiagramMap (fun _ => idmap) (fun _ _ _ _ => 1).
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.