Proposition per_subobject_impl_laws : per_subobject_laws ζ. Proof. unfold ζ. split. - use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (γ := π₂ (tm_var (𝟙 ×h Γ))). fold γ. use weaken_right. apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify_form. rewrite !partial_setoid_subst. simplify. pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h Γ)))). pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ) ×h Γ))). fold γ₁ γ₂. use conj_intro. + use impl_intro. use per_subobject_eq. * exact γ₁. * do 2 use weaken_left. apply hyperdoctrine_hyp. * use impl_elim. ** exact (ψ₁ [ γ₁ ]). ** use per_subobject_eq. *** exact γ₂. *** use partial_setoid_sym. do 2 use weaken_left. apply hyperdoctrine_hyp. *** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use weaken_left. use partial_setoid_refl_r. * exact γ₁. * 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.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.Limits.BinProducts. 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. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Conjunction.