Proposition hyperdoctrine_pair_comp {H : preorder_hyperdoctrine} {Γ Γ' A B : ty H} (s : tm Γ Γ') (t₁ : tm Γ' A) (t₂ : tm Γ' B) : s · ⟨ t₁, t₂ ⟩ = ⟨ s · t₁, s · t₂ ⟩. Proof. apply hyperdoctrine_pair_subst. 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.