Proposition partial_setoid_trans {H : first_order_hyperdoctrine} {X : partial_setoid H} {Γ : ty H} {Δ : form Γ} {x : tm Γ X} (y : tm Γ X) {z : tm Γ X} (p : Δ ⊢ x ~ y) (q : Δ ⊢ y ~ z) : Δ ⊢ x ~ z. Proof. use per_trans. - exact y. - simplify. exact p. - simplify. 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.