is_PO f g (Pushout f g). Proof. srapply Build_IsColimit. - srapply Build_span_cocone. + exact (push o inl). + exact (push o inr). + exact pglue. - srapply Build_UniversalCocone. intro Y; srapply isequiv_adjointify. + intro Co. srapply Pushout_rec. * exact (pol' Co). * exact (por' Co). * exact (popp' Co). + intros [Co Co']. srapply path_cocone. * intros [[]|[]] x; simpl. 1: apply (Co' (inl tt) (inr false) tt). all: reflexivity. * cbn beta. intros [u|b] [u'|b'] [] x. destruct u, b'; cbn. 2: reflexivity. rhs nrapply concat_1p. lhs refine (_ @@ 1). 1: nrapply Pushout_rec_beta_pglue. unfold popp', legs_comm. apply concat_pV_p. + intro h. apply path_forall. srapply Pushout_ind; cbn. 1,2: reflexivity. intro a; cbn beta. nrapply transport_paths_FlFr'; apply equiv_p1_1q. unfold popp'; cbn. rhs_V nrapply concat_p1. nrapply Pushout_rec_beta_pglue. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram. Require Import Diagrams.Span. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Import Colimits.Pushout.