Proposition tripos_to_weak_tripos_law {H : tripos} (X : ty H) : is_weak_tripos_law (tripos_in X). Proof. intros Γ R. use forall_intro. use exists_intro. - exact ({{ R }} [ π₂ (tm_var _) ]tm). - cbn ; simplify. use forall_intro. pose (x := π₂ (tm_var ((𝟙 ×h Γ) ×h X))). pose (γ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h X)))). fold x γ. use iff_intro. + use weaken_right. refine (hyperdoctrine_cut _ (hyperdoctrine_proof_subst ⟨ x , γ ⟩ (mor_to_tripos_power_b X Γ R _ (hyperdoctrine_hyp _)))). rewrite tripos_in_subst. simplify. apply hyperdoctrine_hyp. + use weaken_right. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst ⟨ x , γ ⟩ (mor_to_tripos_power_f X Γ R _ (hyperdoctrine_hyp _))) _). rewrite tripos_in_subst. simplify. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.