{ x : X & Pushout (f x) (g x) } <~> Pushout (functor_sigma idmap f) (functor_sigma idmap g). Proof. srefine (equiv_adjointify esp1 esp2 _ _). - srefine (Pushout_ind _ _ _ _); cbn. + reflexivity. + reflexivity. + intros [x a]. refine (transport_paths_FFlr _ _ @ _). refine (concat_p1 _ @@ 1 @ _). apply moveR_Vp; symmetry. refine (concat_p1 _ @ _). refine (ap _ (esp2_beta_pglue _ _) @ _). apply esp1_beta_pglue. - intros [x a]; revert a. srefine (Pushout_ind _ _ _ _); cbn. + reflexivity. + reflexivity. + intros a. rewrite transport_paths_FlFr. rewrite concat_p1; apply moveR_Vp; rewrite concat_p1. rewrite (ap_compose (exist _ x) (esp2 o esp1)). rewrite (ap_compose esp1 esp2). rewrite (ap_exist (fun x => Pushout (f x) (g x)) x _ _ (pglue a)). rewrite esp1_beta_pglue, esp2_beta_pglue. reflexivity. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.