(D1 D2 : Diagram G) (path_obj : forall i, D1 i = D2 i) (path_arr : forall i j (g : G i j) x, transport idmap (path_obj j) (D1 _f g x) = D2 _f g (transport idmap (path_obj i) x)) : D1 = D2. Proof. srapply path_diagram_naive; funext i. 1: apply path_obj. funext j g x. rewrite 3 transport_forall_constant, transport_arrow. transport_path_forall_hammer. refine (_ @ path_arr i j g (transport idmap (path_obj i)^ x) @ _). { do 3 f_ap. rewrite <- path_forall_V. funext y. by transport_path_forall_hammer. } f_ap. exact (transport_pV idmap _ x). Defined.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.