Definition per_subobject_mor_law {X Y : partial_setoid H} (φ : partial_setoid_morphism X Y) (ψ₁ : per_subobject X) (ψ₂ : per_subobject Y) : UU := let x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h Y))) in let y := π₂ (tm_var ((𝟙 ×h X) ×h Y)) in (⊤ ⊢ ∀h ∀h (φ [ ⟨ x , y ⟩ ] ⇒ ψ₁ [ x ] ⇒ ψ₂ [ y ])).
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.