Proposition morphism_to_equalizer_partial_setoid_laws_eq {Γ : ty H} (w : tm Γ W) (x : tm Γ X) : let s := π₁ (tm_var (Γ ×h Y)) in let y := π₂ (tm_var (Γ ×h Y)) in χ [ ⟨ w , x ⟩ ] ⊢ (∃h (φ [ ⟨ x [ s ]tm , y ⟩ ] ∧ ψ [ ⟨ x [ s ]tm , y ⟩ ])). Proof. cbn. assert (χ [⟨ w, x ⟩] ⊢ x ~ x) as r. { use (partial_setoid_mor_cod_defined χ w x). apply hyperdoctrine_hyp. } use (exists_elim (partial_setoid_mor_hom_exists φ r)). simplify. pose (s := π₁ (tm_var (Γ ×h Y))). pose (y := π₂ (tm_var (Γ ×h Y))). pose (Δ := χ [⟨ w [s ]tm, x [s ]tm ⟩] ∧ φ [⟨ x [s ]tm, y ⟩]). fold s y Δ. use (weaken_cut (from_eq_partial_setoid_morphism_f p (t₁ := w [ s ]tm) (t₂ := y) _)). - cbn. simplify_form. use exists_intro. * exact (x [ s ]tm). * unfold y, Δ. simplify. apply hyperdoctrine_hyp. - cbn. simplify_form. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. rewrite exists_subst. use exists_intro. + exact (π₂ (π₁ (tm_var _))). + unfold Δ, s, y. clear Δ s y. simplify. use conj_intro. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * pose (s := π₁ (π₁ (tm_var ((Γ ×h Y) ×h X)))). pose (y := π₂ (π₁ (tm_var ((Γ ×h Y) ×h X)))). pose (x' := π₂ (tm_var ((Γ ×h Y) ×h X))). fold s y x'. use (partial_setoid_mor_eq_defined ψ). ** exact x'. ** exact y. ** use (partial_setoid_mor_unique_im χ). *** exact (w [ s ]tm). *** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. *** do 2 use weaken_left. apply hyperdoctrine_hyp. ** use (partial_setoid_mor_cod_defined φ (x [ s ]tm)). use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** do 2 use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Equalizers. 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.