Definition is_coequalizer_cod_fib_mor : h --> wφ. Proof. use make_cod_fib_mor. - use (CoequalizerOut coeq). + exact (dom_mor k). + abstract (rewrite <- !comp_in_cod_fib ; exact (maponpaths dom_mor q)). - abstract (use (CoequalizerOutsEq coeq) ; rewrite !assoc ; rewrite (CoequalizerCommutes coeq) ; cbn ; rewrite (mor_eq k), (mor_eq i) ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.