Proposition is_cartesian_per_subobject_subst_mor : is_cartesian (D := disp_cat_per_subobject) per_subobject_subst_mor. Proof. intros W φ' ψ' p ; cbn -[per_subobject_mor_law] in *. use iscontraprop1. - use isaproptotal2. { intro. apply homsets_disp. } intros. apply locally_prop_disp_cat_per_subobject. - simple refine (_ ,, _) ; [ | apply locally_prop_disp_cat_per_subobject ]. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn ; unfold ζ. pose (w := π₂ (π₁ (tm_var ((𝟙 ×h W) ×h Y)))). pose (y := π₂ (tm_var ((𝟙 ×h W) ×h Y))). fold w y. simple refine (exists_elim (partial_setoid_mor_hom_exists φ _) _). + exact y. + use weaken_left. use (partial_setoid_mor_cod_defined φ'). * exact w. * apply hyperdoctrine_hyp. + unfold w, y ; clear w y. simplify. pose (w := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h W) ×h Y) ×h X))))). pose (y := π₂ (π₁ (tm_var (((𝟙 ×h W) ×h Y) ×h X)))). pose (x := π₂ (tm_var (((𝟙 ×h W) ×h Y) ×h X))). fold w x y. use exists_intro. { exact x. } simplify. fold y. use conj_intro. * use weaken_right. apply hyperdoctrine_hyp. * use (per_subobject_mor p). ** exact w. ** cbn. simplify_form. use exists_intro. { exact y. } simplify. use conj_intro. *** do 2 use weaken_left. apply hyperdoctrine_hyp. *** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory.