Proposition exp_partial_setoid_eq_is_function {Γ : ty H} {Δ : form Γ} {f g : tm Γ (ℙ (X ×h Y))} (p : Δ ⊢ exp_partial_setoid_eq [ ⟨ f , g ⟩ ]) (q : Δ ⊢ exp_partial_setoid_is_function [ f ]) : Δ ⊢ exp_partial_setoid_is_function [ g ]. Proof. unfold exp_partial_setoid_is_function. simplify_form. repeat use conj_intro. - unfold exp_partial_setoid_dom_defined_law. simplify_form. do 2 use forall_intro. use impl_intro. simplify_form. rewrite partial_setoid_subst. simplify. pose (γ := π₁ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (x := π₂ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (y := π₂ (tm_var ((Γ ×h X) ×h Y))). fold γ x y. use exp_partial_setoid_dom_defined. + exact (f [ γ ]tm). + exact y. + use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ q) _). simplify. apply hyperdoctrine_hyp. + use (weaken_cut (weaken_left (hyperdoctrine_proof_subst γ p) _) _). use hyp_ltrans. use weaken_right. simplify. use from_exp_partial_setoid_eq. * exact (g [ γ ]tm). * use weaken_right. use exp_partial_setoid_eq_sym. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_cod_defined_law. simplify_form. do 2 use forall_intro. use impl_intro. rewrite partial_setoid_subst. simplify. pose (γ := π₁ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (x := π₂ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (y := π₂ (tm_var ((Γ ×h X) ×h Y))). fold γ x y. use exp_partial_setoid_cod_defined. + exact (f [ γ ]tm). + exact x. + use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ q) _). simplify. apply hyperdoctrine_hyp. + use (weaken_cut (weaken_left (hyperdoctrine_proof_subst γ p) _) _). use hyp_ltrans. use weaken_right. simplify. use from_exp_partial_setoid_eq. * exact (g [ γ ]tm). * use weaken_right. use exp_partial_setoid_eq_sym. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_eq_defined_law. simplify_form. do 4 use forall_intro. do 3 use impl_intro. rewrite !partial_setoid_subst. simplify. pose (γ := π₁ (π₁ (π₁ (π₁ (tm_var ((((Γ ×h X) ×h X) ×h Y) ×h Y)))))). pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((Γ ×h X) ×h X) ×h Y) ×h Y)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var ((((Γ ×h X) ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var ((((Γ ×h X) ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var ((((Γ ×h X) ×h X) ×h Y) ×h Y))). fold γ x₁ x₂ y₁ y₂. use from_exp_partial_setoid_eq. + exact (f [ γ ]tm). + do 3 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ p) _). simplify. apply hyperdoctrine_hyp. + use exp_partial_setoid_eq_defined. * do 3 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ q) _). simplify. apply hyperdoctrine_hyp. * exact x₁. * do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * exact y₁. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * use from_exp_partial_setoid_eq. ** exact (g [ γ ]tm). ** do 3 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ p) _). simplify. use exp_partial_setoid_eq_sym. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_unique_im_law. simplify_form. do 3 use forall_intro. do 2 use impl_intro. simplify_form. rewrite partial_setoid_subst. simplify. pose (γ := π₁ (π₁ (π₁ (tm_var (((Γ ×h X) ×h Y) ×h Y))))). pose (x := π₂ (π₁ (π₁ (tm_var (((Γ ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var (((Γ ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var (((Γ ×h X) ×h Y) ×h Y))). fold γ x y₁ y₂. use exp_partial_setoid_unique_im. + exact (f [ γ ]tm). + do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ q) _). simplify. apply hyperdoctrine_hyp. + exact x. + use from_exp_partial_setoid_eq. * exact (g [ γ ]tm). * do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ p) _). simplify. use exp_partial_setoid_eq_sym. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use from_exp_partial_setoid_eq. * exact (g [ γ ]tm). * do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ p) _). simplify. use exp_partial_setoid_eq_sym. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_im_exists_law. simplify_form. use forall_intro. use impl_intro. rewrite partial_setoid_subst. simplify. pose (γ := π₁ (tm_var (Γ ×h X))). pose (x := π₂ (tm_var (Γ ×h X))). fold γ x. use (exists_elim (exp_partial_setoid_im_exists _ _)). + exact (f [ γ ]tm). + use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ q) _). simplify. apply hyperdoctrine_hyp. + exact x. + use weaken_right. apply hyperdoctrine_hyp. + unfold γ, x ; clear γ x. simplify. pose (γ := π₁ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (x := π₂ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (y := π₂ (tm_var ((Γ ×h X) ×h Y))). fold γ x y. use exists_intro. * exact y. * simplify. fold γ x. use from_exp_partial_setoid_eq. ** exact (f [ γ ]tm). ** do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ p) _). simplify. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms.