Proposition preserves_chosen_subobject_classifier_disp_codomain_fiber_functor_eq : # (fiber_functor (disp_codomain_functor F) x) (cod_fib_subobject_classifier T₁ P₁ Ω₁ x) · preserves_chosen_subobject_classifier_disp_codomain_fiber_functor_iso = TerminalArrow (codomain_fib_terminal (F x)) _ · cod_fib_subobject_classifier T₂ P₂ Ω₂ (F x). Proof. use eq_mor_cod_fib. refine (comp_in_cod_fib _ _ @ _ @ !(comp_in_cod_fib _ _)). rewrite disp_codomain_fiber_functor_mor. cbn. rewrite functor_id. rewrite !id_left. use BinProductArrowsEq. - rewrite !assoc'. rewrite BinProductPr1Commutes. rewrite BinProductOfArrowsPr1. rewrite id_right. rewrite BinProductPr1Commutes. rewrite <- functor_comp, <- functor_id. apply maponpaths. apply BinProductPr1Commutes. - rewrite !assoc'. rewrite BinProductPr2Commutes. rewrite BinProductOfArrowsPr2. etrans. { apply maponpaths. rewrite !assoc. rewrite BinProductPr2Commutes. apply idpath. } rewrite !assoc. rewrite <- functor_comp. etrans. { apply maponpaths_2. apply maponpaths. apply BinProductPr2Commutes. } unfold mor_subobject_classifier, const_true. rewrite functor_comp. rewrite (functor_on_terminal_arrow T₁ HFT x). assert (TerminalArrow (preserves_terminal_to_terminal F HFT T₁) (F x) = TerminalArrow T₂ _ · TerminalArrow (preserves_terminal_to_terminal F HFT T₁) T₂) as q. { apply TerminalArrowEq. } rewrite q. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. exact (subobject_classifier_square_commutes Ω₂ (preserves_subobject_classifier_on_ob HFΩ Ω₁)). } rewrite !assoc. apply maponpaths_2. apply TerminalArrowEq. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.PullbackConstructions. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso. Require Import UniMath.CategoryTheory.SubobjectClassifier.PreservesSubobjectClassifier. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseSubobjectClassifier. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodMorphisms. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. pose (BP := BinProductsFromPullbacks P T). pose (BP := BinProductsFromPullbacks P T).