Definition disp_bicat_of_prod_type : disp_bicat bicat_cat_with_terminal_cleaving. Proof. use disp_subbicat. - exact (λ (C : cat_with_terminal_cleaving), fiberwise_binproducts (cleaving_of_types C)). - exact (λ (C₁ C₂ : cat_with_terminal_cleaving) (T₁ : fiberwise_binproducts (cleaving_of_types C₁)) (T₂ : fiberwise_binproducts (cleaving_of_types C₂)) (F : functor_with_terminal_cleaving C₁ C₂), ∏ (x : C₁), preserves_binproduct (fiber_functor (comp_cat_type_functor F) x)). - abstract (intros C P x y₁ y₂ p π₁ π₂ H ; exact H). - abstract (intros C₁ C₂ C₃ P₁ P₂ P₃ F G HF HG x y₁ y₂ p π₁ π₂ H ; use (isBinProduct_eq_arrow _ _ (composition_preserves_binproduct (HF x) (HG _) _ _ _ _ _ H)) ; cbn ; rewrite disp_functor_transportf ; rewrite transport_f_f ; apply maponpaths_2 ; apply homset_property). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.LiftDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.