Proposition is_univalent_disp_cat_per_subobject : is_univalent_disp disp_cat_per_subobject. Proof. use is_univalent_disp_from_fibers. intros X ψ₁ ψ₂ ; cbn in X, ψ₁, ψ₂. use isweqimplimpl. - intros pq. pose (p := pr1 pq). pose (q := pr12 pq). cbn -[per_subobject_mor_law] in p, q. use subtypePath. { intro. apply isaprop_per_subobject_laws. } use hyperdoctrine_formula_eq. + pose (x := tm_var X). rewrite <- (hyperdoctrine_id_subst (pr1 ψ₁)). rewrite <- (hyperdoctrine_id_subst (pr1 ψ₂)). use (per_subobject_mor p). * apply tm_var. * fold x. cbn. rewrite partial_setoid_subst. simplify. use (per_subobject_def ψ₁). apply hyperdoctrine_hyp. * apply hyperdoctrine_hyp. + pose (x := tm_var X). rewrite <- (hyperdoctrine_id_subst (pr1 ψ₁)). rewrite <- (hyperdoctrine_id_subst (pr1 ψ₂)). use (per_subobject_mor q). * apply tm_var. * fold x. cbn. rewrite partial_setoid_subst. simplify. use (per_subobject_def ψ₂). apply hyperdoctrine_hyp. * apply hyperdoctrine_hyp. - apply isaset_per_subobject. - use isaproptotal2. + intro. apply isaprop_is_z_iso_disp. + intros. apply isaprop_per_subobject_mor_law. 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.