{D1 D2 : Diagram G} {m1 m2 : DiagramMap D1 D2} (h_obj : forall i, m1 i == m2 i) (h_comm : forall i j (g : G i j) x, DiagramMap_comm m1 g x @ h_obj j (D1 _f g x) = ap (D2 _f g) (h_obj i x) @ DiagramMap_comm m2 g x) : m1 = m2. Proof. destruct m1 as [m1_obj m1_comm]. destruct m2 as [m2_obj m2_comm]. simpl in *. revert h_obj h_comm. set (E := (@equiv_functor_forall _ G (fun i => m1_obj i = m2_obj i) G (fun i => m1_obj i == m2_obj i) idmap _ (fun i => @apD10 _ _ (m1_obj i) (m2_obj i))) (fun i => isequiv_apD10 _ _ _ _)). equiv_intro E h_obj. revert h_obj. equiv_intro (@apD10 _ _ m1_obj m2_obj) h_obj. destruct h_obj; simpl. intros h_comm. assert (HH : m1_comm = m2_comm). { funext i j f x. apply (concatR (concat_1p _)). apply (concatR (h_comm _ _ _ _)). apply inverse, concat_p1. } destruct HH. reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.