{A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'} (a : A $<~> A') (b : B $<~> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g) : ab_coeq f g $<~> ab_coeq f' g'. Proof. snrapply cate_adjointify. - exact (functor_ab_coeq a b p q). - exact (functor_ab_coeq a^-1$ b^-1$ (hinverse _ _ p) (hinverse _ _ q)). - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _ $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _). rapply cate_isretr. - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _ $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _). rapply cate_issect. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.