Proposition proof_to_partial_setoid_morphism_eq {Γ₁ Γ₂ : ty H} {Δ : form Γ₁} {φ : form Γ₂} {s : tm Γ₁ Γ₂} (q : Δ ⊢ φ [ s ]) : partial_setoid_comp_morphism (proof_to_partial_setoid_morphism q) (formula_to_partial_setoid_incl φ) = partial_setoid_comp_morphism (formula_to_partial_setoid_incl Δ) (term_partial_setoid_morphism s). Proof. use eq_partial_setoid_morphism. - use (exists_elim (hyperdoctrine_hyp _)) ; cbn. use weaken_right. simplify_form. use exists_intro. + exact (π₁ (π₁ (tm_var _))). + simplify. pose (x := π₁ (π₁ (tm_var ((Γ₁ ×h Γ₂) ×h Γ₂)))). pose (y₁ := π₂ (π₁ (tm_var ((Γ₁ ×h Γ₂) ×h Γ₂)))). pose (y₂ := π₂ (tm_var ((Γ₁ ×h Γ₂) ×h Γ₂))). fold x y₁ y₂. use conj_intro. * use conj_intro. ** apply hyperdoctrine_refl. ** do 2 use weaken_left. apply hyperdoctrine_hyp. * use hyperdoctrine_eq_trans. ** exact y₂. ** use hyperdoctrine_eq_sym. use weaken_left. do 2 use weaken_right. apply hyperdoctrine_hyp. ** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. - use (exists_elim (hyperdoctrine_hyp _)) ; cbn. use weaken_right. simplify_form. use exists_intro. + exact (π₂ (π₁ (tm_var _))). + simplify. pose (x₁ := π₁ (π₁ (tm_var ((Γ₁ ×h Γ₂) ×h Γ₁)))). pose (y := π₂ (π₁ (tm_var ((Γ₁ ×h Γ₂) ×h Γ₁)))). pose (x₂ := π₂ (tm_var ((Γ₁ ×h Γ₂) ×h Γ₁))). fold x₁ x₂ y. assert ((x₁ ≡ x₂ ∧ Δ [x₁]) ∧ s [x₂ ]tm ≡ y ⊢ φ [y]) as r. { refine (weaken_cut (weaken_left (weaken_right (hyperdoctrine_proof_subst x₁ q) _) _) _). simplify. use hyperdoctrine_eq_transportf. * exact (s [ x₁ ]tm). * use weaken_left. refine (hyperdoctrine_eq_trans _ (weaken_right (hyperdoctrine_hyp _) _)). do 2 use weaken_left. use hyperdoctrine_subst_eq. use hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. } use conj_intro. * use conj_intro. ** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** use conj_intro. *** exact r. *** use hyperdoctrine_eq_trans. **** exact (s [ x₂ ]tm). **** use hyperdoctrine_eq_sym. use weaken_right. apply hyperdoctrine_hyp. **** use hyperdoctrine_subst_eq. use hyperdoctrine_eq_sym. do 2 use weaken_left. apply hyperdoctrine_hyp. * use conj_intro. ** apply hyperdoctrine_refl. ** exact r. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. 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.PERConstantObjects.