proposition: Lemma diagram_equiv_inv {D1 D2 : Diagram G} (w : diagram_equiv D1 D2) : DiagramMap D2 D1.
proof: Proof. apply (Build_DiagramMap (fun i => (Build_Equiv _ _ _ (diag_equiv_isequiv w i))^-1)). intros i j f. apply (@comm_square_inverse _ _ _ _ _ _ (Build_Equiv _ _ _ (diag_equiv_isequiv w i)) (Build_Equiv _ _ _ (diag_equiv_isequiv w j))). intros x; apply DiagramMap_comm. Defined.
imports: Basics Types HoTT.Tactics Diagrams.CommutativeSquares Diagrams.Graph