Definition exp_in_fiber_locally_propositional (Γ : C) : Exponentials (pr1 P Γ). Proof. intros φ. use left_adjoint_from_partial. - exact (λ ψ, imp _ φ ψ). - exact (λ ψ, imp_e _ φ ψ). - intros ψ χ p. use iscontraprop1. + abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; apply HD'). + simple refine (_ ,, _) ; [ | apply HD' ]. apply imp_i. exact p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. 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.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.exponentials.