Definition fiberwise_subobject_classifier {C : category} {D : disp_cat C} {HD : cleaving D} (TD : fiberwise_terminal HD) : UU := (∏ (x : C), subobject_classifier (terminal_in_fib TD x)) × (∏ (x y : C) (f : x --> y), preserves_subobject_classifier (fiber_functor_from_cleaving D HD f) (terminal_in_fib TD y) (terminal_in_fib TD x) (preserves_terminal_in_fib TD f)).
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.