Proposition hyperdoctrine_pair_comp_pr2 {H : preorder_hyperdoctrine} {Γ A B : ty H} (t₁ : tm Γ A) (t₂ : tm Γ B) : (π₂ (tm_var _)) [ ⟨ t₁ , t₂ ⟩ ]tm = t₂. Proof. rewrite hyperdoctrine_pr2_subst. unfold tm_subst. rewrite id_right. rewrite hyperdoctrine_pair_pr2. apply idpath. 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.