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