Definition mono_codomain_fib_binproducts_prod : isBinProduct (C /m x) _ _ _ π₁ π₂. Proof. intros h φ ψ. use iscontraprop1. - abstract (use isaproptotal2 ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; intros ; apply locally_propositional_mono_cod_disp_cat). - simple refine ((_ ,, tt) ,, _ ,, _). + exact (BinProductArrow _ P (#(mono_cod_to_cod_fib _) φ) (#(mono_cod_to_cod_fib _) ψ)). + apply locally_propositional_mono_cod_disp_cat. + apply locally_propositional_mono_cod_disp_cat. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.Inclusion.