(D1 D2 : Diagram G) := { DiagramMap_obj :> forall i, D1 i -> D2 i; DiagramMap_comm : forall i j (g: G i j) x, D2 _f g (DiagramMap_obj i x) = DiagramMap_obj j (D1 _f g x) }.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.