Proposition preserves_chosen_to_preserves_subobject_classifier {C₁ C₂ : univalent_category} {F : C₁ ⟶ C₂} {T₁ : Terminal C₁} {T₂ : Terminal C₂} {HF : preserves_terminal F} {Ω : subobject_classifier T₁} (HF' : preserves_chosen_subobject_classifier F T₁ T₂ HF Ω) : preserves_subobject_classifier F T₁ T₂ HF. Proof. intros O' t H. pose (Ω' := (O' ,, t ,, H) : subobject_classifier T₁). pose (f := z_iso_subobject_classifier Ω Ω'). use z_iso_to_is_subobject_classifier. - exact (F Ω ,, TerminalArrow (preserves_terminal_to_terminal F HF T₁) _ · #F (true Ω) ,, HF'). - exact (functor_on_z_iso F f). - cbn. rewrite !assoc'. rewrite <- functor_comp. unfold mor_subobject_classifier. etrans. { do 2 apply maponpaths. exact (subobject_classifier_square_commutes Ω' (true Ω)). } rewrite functor_comp. rewrite !assoc. apply maponpaths_2. apply (TerminalArrowEq (T := preserves_terminal_to_terminal F HF T₁)). 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.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso.