{A B : Type} (p : forall b:B, b = b) (g : A <~> B) : equiv_path2_universe g g (fun a => (p (g a))) = (concat_p1 _)^ @ whiskerL (path_universe g) (path_universe_1)^ @ whiskerL (path_universe g) (equiv_path2_universe (equiv_idmap B) (equiv_idmap B) p) @ whiskerL (path_universe g) (path_universe_1) @ concat_p1 _. Proof. transitivity ((eta_path_universe (path_universe g))^ @ equiv_path2_universe (equiv_path A B (path_universe g)) (equiv_path A B (path_universe g)) (fun a => p (equiv_path A B (path_universe g) a)) @ eta_path_universe (path_universe g)). - refine ((apD (fun g' => equiv_path2_universe g' g' (fun a => p (g' a))) (eisretr (equiv_path A B) g))^ @ _). refine (transport_paths_FlFr (eisretr (equiv_path A B) g) _ @ _). apply concat2. + apply whiskerR. apply inverse2, symmetry. refine (eisadj (equiv_path A B)^-1 g). + symmetry; refine (eisadj (equiv_path A B)^-1 g). - generalize (path_universe g). intros h. destruct h. cbn. rewrite !concat_p1. refine (_ @ (((concat_1p (whiskerL 1 path_universe_1^))^ @@ 1) @@ 1)). refine (_ @ whiskerR (whiskerL_pp 1 path_universe_1^ _) _). refine (_ @ whiskerL_pp 1 _ path_universe_1). exact ((whiskerL_1p_1 _)^). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.