Definition is_cowedge (w : cowedge_data) : UU := ∏ (x y : C) (g : x --> y), #F (catbinprodmor (identity _) g) · mor_of_cowedge w y = #F (catbinprodmor g (identity _)) · mor_of_cowedge w x.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers.