proposition: Lemma diagram_inv_is_section {D1 D2 : Diagram G} (w : diagram_equiv D1 D2) : diagram_comp w (diagram_equiv_inv w) = diagram_idmap D2.
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 => eisretr (we i)). - simpl. intros i j f x. apply (concatR (concat_p1 _)^). apply (comm_square_inverse_is_retr (we i) (we j) _ x). Defined.
imports: Basics Types HoTT.Tactics Diagrams.CommutativeSquares Diagrams.Graph