{B A} {f g : B -> A} : (Coeq_sym_map f g) o (Coeq_sym_map g f) == idmap. Proof. srapply @Coeq_ind. - reflexivity. - intro b. simpl. abstract (rewrite transport_paths_FFlr, Coeq_rec_beta_cglue, ap_V, Coeq_rec_beta_cglue; hott_simpl). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.