proposition: Lemma iscoequalizer_Coeq `{Funext} : IsColimit (parallel_pair f g) (Coeq f g).
proof: Proof. srapply (Build_IsColimit cocone_Coeq). srapply Build_UniversalCocone. intros X. srapply isequiv_adjointify. - intros C. srapply Coeq_rec. + exact (legs C false). + intros b. etransitivity. * exact (legs_comm C true false true b). * exact (legs_comm C true false false b)^. - intros C. srapply path_cocone. + intros i x; destruct i; simpl. * exact (legs_comm C true false false x). * reflexivity. + intros i j phi x; destruct i, j, phi; simpl. * hott_simpl. match goal with | [|- ap (Coeq_rec ?a ?b ?c) _ @ _ = _ ] => rewrite (Coeq_rec_beta_cglue a b c) end. hott_simpl. * reflexivity. - intros F. apply path_forall. match goal with | [|- ?G == _ ] => simple refine (Coeq_ind (fun w => G w = F w) _ _) end. + reflexivity. + intros b; simpl. nrapply (transport_paths_FlFr' (g:=F)). apply equiv_p1_1q. refine (Coeq_rec_beta_cglue _ _ _ _ @ _). apply concat_p1. Defined.
imports: Basics Types Diagrams.ParallelPair Diagrams.Cocone Colimits.Colimit Colimits.Coeq