Proposition functor_to_partial_setoids_laws : is_functor functor_to_partial_setoids_data. Proof. split. - refine (λ (X : ty H), _). use eq_partial_setoid_morphism ; cbn in *. + use eq_in_eq_partial_setoid. use (hyperdoctrine_eq_trans _ (hyperdoctrine_hyp _)). use hyperdoctrine_refl_eq. refine (!_). exact (var_tm_subst (π₁ (tm_var (X ×h X)))). + use (hyperdoctrine_cut (from_eq_in_eq_partial_setoid (hyperdoctrine_hyp _))). use (hyperdoctrine_eq_trans _ (hyperdoctrine_hyp _)). use hyperdoctrine_refl_eq. exact (var_tm_subst (π₁ (tm_var (X ×h X)))). - refine (λ (X Y Z : ty H) (t₁ : tm X Y) (t₂ : tm Y Z), _). use eq_partial_setoid_morphism ; cbn in *. + use exists_intro. * exact (t₁ [ π₁ (tm_var _) ]tm). * simplify. use conj_intro. ** apply hyperdoctrine_refl. ** use (hyperdoctrine_eq_trans _ (hyperdoctrine_hyp _)). use hyperdoctrine_refl_eq. exact (!(tm_subst_comp (π₁ (tm_var (X ×h Z))) t₁ t₂)). + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. use (hyperdoctrine_eq_trans _ (weaken_right (hyperdoctrine_hyp _) _)). use weaken_left. use hyperdoctrine_eq_trans. * exact (t₂ [ t₁ [π₁ (π₁ (tm_var ((X ×h Z) ×h Y))) ]tm ]tm). * use hyperdoctrine_refl_eq. exact (tm_subst_comp _ t₁ t₂). * use hyperdoctrine_subst_eq. 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.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory.