Proposition isaprop_fiberwise_subobject_classifier {C : category} {D : disp_univalent_category C} {HD : cleaving D} (TD : fiberwise_terminal HD) : isaprop (fiberwise_subobject_classifier TD). Proof. use isapropdirprod. - use impred ; intro. apply isaprop_subobject_classifier'. use is_univalent_fiber. apply disp_univalent_category_is_univalent_disp. - do 3 (use impred ; intro). apply isaprop_preserves_subobject_classifier. Qed.
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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso. Require Import UniMath.CategoryTheory.SubobjectClassifier.PreservesSubobjectClassifier.