Proposition exp_partial_setoid_cod_defined {Γ : ty H} {Δ : form Γ} {f : tm Γ (ℙ (X ×h Y))} {x : tm Γ X} {y : tm Γ Y} (p : Δ ⊢ exp_partial_setoid_is_function [ f ]) (q : Δ ⊢ ⟨ x , y ⟩ ∈ f) : Δ ⊢ y ~ y. Proof. unfold exp_partial_setoid_is_function in p. rewrite !conj_subst in p. pose proof (r := conj_elim_left (conj_elim_right p)). clear p. unfold exp_partial_setoid_cod_defined_law in r. rewrite !forall_subst in r. pose proof (r' := forall_elim r x). clear r ; rename r' into r. rewrite forall_subst in r. pose proof (r' := forall_elim r y). clear r ; rename r' into r. refine (weaken_cut r _). simplify_form. rewrite partial_setoid_subst. simplify. refine (impl_elim _ (weaken_right (hyperdoctrine_hyp _) _)). use weaken_left. exact q. 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.