{D1 D2 D3 : Diagram G} (m2 : DiagramMap D2 D3) (m1 : DiagramMap D1 D2) : DiagramMap D1 D3. Proof. apply (Build_DiagramMap (fun i => m2 i o m1 i)). intros i j f. exact (comm_square_comp (DiagramMap_comm m1 f) (DiagramMap_comm m2 f)). Defined.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.