{D1 D2 : Diagram G} (w : diagram_equiv D1 D2) : diagram_comp (diagram_equiv_inv w) w = diagram_idmap D1. Proof. destruct w as [[w_obj w_comm] is_eq_w]. simpl in *. set (we i := Build_Equiv _ _ _ (is_eq_w i)). simple refine (path_DiagramMap _ _). - exact (fun i => eissect (we i)). - simpl. intros i j f x. apply (concatR (concat_p1 _)^). apply (comm_square_inverse_is_sect (we i) (we j) _ x). Defined.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.