Definition is_dispBinProduct_naive (c d p : C) (p1 : p --> c) (p2 : p --> d) (cc : D c) (dd : D d) (pp : D p) (pp1 : pp -->[p1] cc) (pp2 : pp -->[p2] dd) : UU := ∏ (a : C) (f : a --> c) (g : a --> d) (aa : D a) (ff : aa -->[f] cc) (gg : aa -->[g] dd), ∃! (fg : a --> p) (fgfg : aa -->[fg] pp), ∑ fgok : ((fg · p1 = f) × (fg · p2 = g)), (fgfg ;; pp1 = transportb _ (pr1 fgok) ff) × (fgfg ;; pp2 = transportb _ (pr2 fgok) gg).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.