Proposition per_subobject_impl_subst {Γ₁ Γ₂ : partial_setoid H} (s : partial_setoid_morphism Γ₁ Γ₂) (ψ₁ ψ₂ : per_subobject Γ₂) : per_subobject_mor_law (id_partial_setoid_morphism Γ₁) (per_subobject_impl (per_subobject_subst s ψ₁) (per_subobject_subst s ψ₂)) (per_subobject_subst s (per_subobject_impl ψ₁ ψ₂)). Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use hyp_sym. cbn. simplify_form. rewrite !partial_setoid_subst. simplify. simple refine (exists_elim (partial_setoid_mor_hom_exists s _) _). - exact (π₂ (π₁ (tm_var ((𝟙 ×h Γ₁) ×h Γ₁)))). - use weaken_left. use weaken_right. apply hyperdoctrine_hyp. - simplify_form. rewrite !partial_setoid_subst. simplify. pose (γ₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂))))). pose (γ₁' := π₂ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂)))). pose (γ₂ := π₂ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂))). fold γ₁ γ₁' γ₂. use exists_intro. + exact γ₂. + simplify_form. rewrite !partial_setoid_subst. simplify. fold γ₁' γ₂. repeat (use conj_intro). * use hyp_ltrans. use weaken_right. use partial_setoid_mor_eq_defined. ** exact γ₁. ** exact γ₂. ** use weaken_left. apply hyperdoctrine_hyp. ** use (partial_setoid_mor_cod_defined s γ₁). use weaken_right. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. * use impl_intro. do 3 use hyp_ltrans. refine (weaken_cut _ _). { use (impl_elim _ (weaken_left (hyperdoctrine_hyp _) _)). use (exists_intro). { exact γ₂. } simplify. fold γ₁. do 3 use weaken_right. apply hyperdoctrine_hyp. } use hyp_ltrans. use weaken_right. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. unfold γ₁, γ₁', γ₂ ; clear γ₁ γ₁' γ₂. simplify_form. rewrite !partial_setoid_subst. simplify. pose (γ₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂)))))). pose (γ₁' := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂))))). pose (γ₂ := π₂ (π₁ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂)))). pose (γ₂' := π₂ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂))). fold γ₁ γ₁' γ₂ γ₂'. use per_subobject_eq. ** exact γ₂'. ** use (partial_setoid_mor_unique_im s). *** exact γ₁. *** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. *** use weaken_left. do 2 use weaken_right. use weaken_left. apply hyperdoctrine_hyp. ** do 2 use weaken_right. apply hyperdoctrine_hyp. * use weaken_right. use (partial_setoid_mor_cod_defined s). ** 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.