proposition: Lemma sect_Coeq_sym_map {B A} {f g : B -> A} : (Coeq_sym_map f g) o (Coeq_sym_map g f) == idmap.
proof: 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.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod Cubical.DPath Colimits.GraphQuotient