PO (functor_sigma f f0) (functor_sigma g g0) <~> exists x, POCase_P x. Proof. transitivity (Colimit (diagram_sigma POCase_E)). { apply equiv_path. unfold PO; apply ap. srapply path_diagram; cbn. - intros [|[]]; cbn. all: reflexivity. - intros [[]|[]] [[]|[]] [] x; cbn in *. all: reflexivity. } transitivity (exists x, E' (span f g) POCase_E POCase_HE x). - apply flattening_lemma. - apply equiv_functor_sigma_id. intro x. apply equiv_path. unfold E', POCase_P, PO_rec. f_ap. srapply path_cocone. + intros [[]|[]] y; cbn. 1: apply path_universe_uncurried; apply g0. all: reflexivity. + intros [[]|[]] [[]|[]] []; cbn. * intro y. simpl. rhs nrapply concat_1p. unfold path_universe. lhs nrapply (ap (fun x => x @ _) _^). 1: nrapply path_universe_V_uncurried. exact (path_universe_compose (f0 y)^-1 (g0 y))^. * intros; apply concat_Vp. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.DDiagram. Require Import Diagrams.Span. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Colimits.Colimit_Pushout. Require Import Colimits.Colimit_Flattening.