Definition disp_bicat_finlim_subobject_classifier : disp_bicat bicat_of_univ_cat_with_finlim. Proof. use disp_subbicat. - exact (λ (C : univ_cat_with_finlim), subobject_classifier (terminal_univ_cat_with_finlim C)). - exact (λ (C₁ C₂ : univ_cat_with_finlim) (Ω₁ : subobject_classifier (terminal_univ_cat_with_finlim C₁)) (Ω₂ : subobject_classifier (terminal_univ_cat_with_finlim C₂)) (F : functor_finlim C₁ C₂), preserves_subobject_classifier F (terminal_univ_cat_with_finlim C₁) (terminal_univ_cat_with_finlim C₂) (functor_finlim_preserves_terminal F)). - intros. apply identity_preserves_subobject_classifier. - intros C₁ C₂ C₃ Ω₁ Ω₂ Ω₃ F G HF HG. exact (comp_preserves_subobject_classifier HF HG). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.PullbackConstructions. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.PreservationProperties. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.LocallyCartesianClosed.LocallyCartesianClosed. Require Import UniMath.CategoryTheory.LocallyCartesianClosed.Preservation. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso. Require Import UniMath.CategoryTheory.SubobjectClassifier.PreservesSubobjectClassifier. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. := BinProductsFromPullbacks