(a : A) : ap equiv_pushout_PO (pglue a) = popp a. Proof. cbn. refine (_ @ _). 1: nrapply Pushout_rec_beta_pglue. unfold popp'; cbn. rewrite 2 concat_1p. reflexivity. 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.