(D1 D2 : Diagram G) (P := fun D' => forall i j, G i j -> (D' i -> D' j)) (path_obj : obj D1 = obj D2) (path_arr : transport P path_obj (arr D1) = arr D2) : D1 = D2 := match path_arr in (_ = v1) return D1 = {|obj := obj D2; arr := v1 |} with | idpath => match path_obj in (_ = v0) return D1 = {|obj := v0; arr := path_obj # (arr D1) |} with | idpath => 1 end end.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.