fact: Definition path_diagram (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.
imports: Basics Types HoTT.Tactics Diagrams.CommutativeSquares Diagrams.Graph