Proposition hyperdoctrine_pair_subst {H : preorder_hyperdoctrine} {Γ Γ' A B : ty H} (s : tm Γ Γ') (t₁ : tm Γ' A) (t₂ : tm Γ' B) : ⟨ t₁ , t₂ ⟩ [ s ]tm = ⟨ t₁ [ s ]tm , t₂ [ s ]tm ⟩. Proof. unfold hyperdoctrine_pair. apply precompWithBinProductArrow. 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.