Definition mono_codomain_fib_binproducts (x : C) : BinProducts (C /m x). Proof. intros fy₁ fy₂. pose (fy₁' := mono_cod_dom fy₁ ,, pr1 (mono_cod_mor fy₁) : C / x). pose (fy₂' := mono_cod_dom fy₂ ,, pr1 (mono_cod_mor fy₂) : C / x). pose (P := codomain_fib_binproducts HC x fy₁' fy₂'). use make_BinProduct. - use make_mono_cod_fib_ob. + exact (cod_dom P). + use (make_Monic _ (cod_mor P)). abstract (use isMonic_comp ; [ | apply (MonicisMonic _ (monic_of_mono_in_cat fy₁)) ] ; apply (MonicPullbackisMonic' _ _ (monic_of_mono_in_cat fy₂))). - exact (BinProductPr1 _ P ,, tt). - exact (BinProductPr2 _ P ,, tt). - apply mono_codomain_fib_binproducts_prod. apply isBinProduct_BinProduct. 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.