proposition: Lemma Coeq_sym {B A} {f g : B -> A} : @Coeq B A f g <~> Coeq g f.
proof: Proof. exact (equiv_adjointify (Coeq_sym_map f g) (Coeq_sym_map g f) sect_Coeq_sym_map sect_Coeq_sym_map). Defined.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod Cubical.DPath Colimits.GraphQuotient