more direct proof for PO_flattening

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

theories/Colimits/Colimit_Pushout_Flattening.v

@@ -49,31 +49,46 @@ Section POCase.
   Definition PO_flattening
     : PO (functor_sigma f f0) (functor_sigma g g0) <~> exists x, POCase_P x.
   Proof.
-    assert (PO (functor_sigma f f0) (functor_sigma g g0)
-            = Colimit (diagram_sigma POCase_E)). {
-      unfold PO; apply ap.
+    transitivity (Colimit (diagram_sigma POCase_E)).
+    { apply (equiv_transport Colimit).
       srapply path_diagram; cbn.
       - intros [|[]]; cbn. all: reflexivity.
       - intros [[]|[]] [[]|[]] [] x; cbn in *.
-        all: reflexivity. }
-    rewrite X; clear X.
+        all: reflexivity. } 
     transitivity (exists x, E' (span f g) POCase_E POCase_HE x).
     - apply flattening_lemma.
     - apply equiv_functor_sigma_id.
       intro x.
-      assert (E' (span f g) POCase_E POCase_HE x = POCase_P x). {
-        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; hott_simpl.
-            unfold path_universe.
-            rewrite <- path_universe_V_uncurried.
-            refine (path_universe_compose (f0 y)^-1 (g0 y))^. 
-          + intros; apply concat_Vp. }
-      rewrite X. reflexivity.
+      snrapply Build_Equiv.
+      + revert x.
+        snrapply PO_ind.
+        1,2: intro; exact idmap.
+        intros x.
+        apply dpath_arrow.
+        intros y.
+        lhs nrapply transport_idmap_ap.
+        lhs nrapply ap011.
+        1: reflexivity.
+        1: apply PO_rec_beta_pp.
+        lhs nrapply transport_path_universe_uncurried.
+        unfold popp.
+        rhs nrapply (transport_pp (E' (span f g) POCase_E POCase_HE)
+          (colimp (D:=span f g) (inl tt) (inr true) tt x)
+          (colimp (D:=span f g) (inl tt) (inr false) tt x)^).
+        rhs nrapply (transport_E'_V (span f g) POCase_E POCase_HE
+          (i:=inl tt) (j:=inr false)).
+        simpl; f_ap.
+        rhs nrapply ap011.
+        2: exact (eisretr (f0 x) y)^.  
+        2: reflexivity.
+        symmetry.
+        exact (transport_E' (span f g) POCase_E POCase_HE
+          (i:=inl tt) (j:=inr true) tt x ((f0 x)^-1 y)).
+      + revert x.
+        snrapply PO_ind.
+        1,2: intro; apply isequiv_idmap.
+        intro x.
+        apply path_ishprop.
   Defined.
 
 End POCase.