Proposition id_preserves_locally_cartesian_closed {C : category} {PB : Pullbacks C} (H : is_locally_cartesian_closed PB) : preserves_locally_cartesian_closed (identity_preserves_pullback C) H H. Proof. unfold preserves_locally_cartesian_closed. refine (transportf (λ z, preserves_dependent_products z _ _) _ (id_preserves_dependent_products (cod_dependent_products H))). use subtypePath. { intro. apply isaprop_is_cartesian_disp_functor. } use subtypePath. { intro. apply isaprop_disp_functor_axioms. } use total2_paths_f. - apply idpath. - cbn. repeat (use funextsec ; intro). use eq_cod_mor ; cbn. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.LocallyCartesianClosed.LocallyCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodRightAdjoint. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.