Proposition omega_partial_setoid_true_laws : partial_setoid_morphism_laws omega_partial_setoid_true_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. pose (ω := π₂ (tm_var (((𝟙 : ty H) ×h 𝟙) ×h Ω))). pose (t₁ := π₂ (π₁ (tm_var (((𝟙 : ty H) ×h 𝟙) ×h Ω)))). pose (t₂ := π₁ (π₁ (tm_var (((𝟙 : ty H) ×h 𝟙) ×h Ω)))). fold ω t₁ t₂. use eq_in_eq_partial_setoid. use hyperdoctrine_unit_tm_eq. - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. pose (ω := π₂ (tm_var (((𝟙 : ty H) ×h 𝟙) ×h Ω))). pose (t₁ := π₂ (π₁ (tm_var (((𝟙 : ty H) ×h 𝟙) ×h Ω)))). pose (t₂ := π₁ (π₁ (tm_var (((𝟙 : ty H) ×h 𝟙) ×h Ω)))). fold ω t₁ t₂. use eq_in_omega_partial_setoid. apply iff_refl. - unfold partial_setoid_mor_eq_defined_law ; cbn. do 4 (use forall_intro). use impl_intro. use weaken_right. do 2 use impl_intro. simplify. pose (t₁ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 : ty H) ×h 𝟙) ×h 𝟙) ×h Ω) ×h Ω)))))). pose (t₂ := π₂ (π₁ (π₁ (tm_var (((((𝟙 : ty H) ×h 𝟙) ×h 𝟙) ×h Ω) ×h Ω))))). pose (ω₁ := π₂ (π₁ (tm_var (((((𝟙 : ty H) ×h 𝟙) ×h 𝟙) ×h Ω) ×h Ω)))). pose (ω₂ := π₂ (tm_var (((((𝟙 : ty H) ×h 𝟙) ×h 𝟙) ×h Ω) ×h Ω))). fold t₁ t₂ ω₁ ω₂. use hyp_ltrans. use weaken_right. use iff_elim_left. + exact (Prf [ ω₁ ]). + use weaken_left. use from_eq_in_omega_partial_setoid. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify. pose (ω₁ := π₂ (π₁ (tm_var ((((𝟙 : ty H) ×h 𝟙) ×h Ω) ×h Ω)))). pose (ω₂ := π₂ (tm_var ((((𝟙 : ty H) ×h 𝟙) ×h Ω) ×h Ω))). fold ω₁ ω₂. use eq_in_omega_partial_setoid. use iff_true_true. + use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law ; cbn. use forall_intro. use impl_intro. use weaken_right. pose (t₁ := π₁ (tm_var ((𝟙 : ty H) ×h 𝟙))). pose (t₂ := π₂ (tm_var ((𝟙 : ty H) ×h 𝟙))). use exists_intro. { exact (tripos_form_to_tm ⊤). } simplify. fold t₁ t₂. rewrite tripos_form_to_tm_Prf. apply truth_intro. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. 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. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERTerminal. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms.