Pushout (pushr' f1 g1 o f2) g2 <~> Pushout f1 (pushl' f2 g2 o g1). Proof. srefine (equiv_adjointify _ _ _ _). - exact (pushout_assoc_left_rec _ pushrl pushrm pushrr pgluerl pgluerr). - exact (pushout_assoc_right_rec _ pushll pushlm pushlr pgluell pgluelr). - abstract ( srefine (pushout_assoc_right_ind _ (fun _ => 1) (fun _ => 1) (fun _ => 1) _ _); intros; simpl; rewrite transport_paths_FlFr, ap_compose; [ rewrite pushout_assoc_right_rec_beta_pgluerl, pushout_assoc_left_rec_beta_pgluell | rewrite pushout_assoc_right_rec_beta_pgluerr, pushout_assoc_left_rec_beta_pgluelr ]; rewrite concat_p1, ap_idmap; apply concat_Vp ). - abstract ( srefine (pushout_assoc_left_ind _ (fun _ => 1) (fun _ => 1) (fun _ => 1) _ _); intros; simpl; rewrite transport_paths_FlFr, ap_compose; [ rewrite pushout_assoc_left_rec_beta_pgluell, pushout_assoc_right_rec_beta_pgluerl | rewrite pushout_assoc_left_rec_beta_pgluelr, pushout_assoc_right_rec_beta_pgluerr ]; rewrite concat_p1, ap_idmap; apply concat_Vp ). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.