proposition: Lemma diagram_inv_is_retraction {D1 D2 : Diagram G} (w : diagram_equiv D1 D2) : diagram_comp (diagram_equiv_inv w) w = diagram_idmap D1.
proof: 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.
imports: Basics Types HoTT.Tactics Diagrams.CommutativeSquares Diagrams.Graph