Proposition mono_codomain_fib_preserves_binproduct {x y : C} (f : x --> y) : preserves_binproduct (mono_cod_pb HC f). Proof. use preserves_binproduct_if_preserves_chosen. { apply mono_codomain_fib_binproducts. } intros m₁ m₂. pose (π₁ := BinProductPr1 (C /m y) (mono_codomain_fib_binproducts y m₁ m₂)). pose (π₂ := BinProductPr2 (C /m y) (mono_codomain_fib_binproducts y m₁ m₂)). pose (π₁' := #(mono_cod_to_cod_fib _) π₁). pose (π₂' := #(mono_cod_to_cod_fib _) π₂). Locate mono_cod_fiber_functor_on_mor. rewrite !mono_cod_fiber_functor_on_mor. use mono_codomain_fib_binproducts_prod. use codomain_fib_preserves_binproduct. apply isBinProduct_BinProduct. Qed.
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.