Definition quantifier_subst_pb {H : first_order_hyperdoctrine} {Γ₁ Γ₂ : ty H} (A : ty H) (s : tm Γ₁ Γ₂) : isPullback (!(quantifier_subst_pb_eq A s)). Proof. intros Γ' t t' p. use iscontraprop1. - abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; refine (hyperdoctrine_pair_eta _ @ _ @ !(hyperdoctrine_pair_eta _)) ; pose (pr22 ζ₁) as q ; rewrite hyperdoctrine_pr1_comp in q ; rewrite id_right in q ; rewrite q ; clear q ; pose (pr22 ζ₂) as q ; rewrite hyperdoctrine_pr1_comp in q ; rewrite id_right in q ; rewrite q ; clear q ; apply maponpaths ; pose (maponpaths (λ z, π₂ z) (pr12 ζ₁)) as q ; cbn in q ; rewrite (hyperdoctrine_pair_comp (H := H)) in q ; unfold tm_subst in q ; rewrite !assoc in q ; rewrite (hyperdoctrine_pr1_comp (H := H)) in q ; rewrite hyperdoctrine_pr2_comp in q ; rewrite !id_right in q ; rewrite hyperdoctrine_pair_pr2 in q ; rewrite q ; clear q ; pose (maponpaths (λ z, π₂ z) (pr12 ζ₂)) as q ; cbn in q ; rewrite (hyperdoctrine_pair_comp (H := H)) in q ; unfold tm_subst in q ; rewrite !assoc in q ; rewrite (hyperdoctrine_pr1_comp (H := H)) in q ; rewrite hyperdoctrine_pr2_comp in q ; rewrite !id_right in q ; rewrite hyperdoctrine_pair_pr2 in q ; rewrite q ; clear q ; apply idpath). - refine (⟨ t' , t · π₂ (tm_var _) ⟩ ,, _ ,, _). + abstract (rewrite hyperdoctrine_pair_comp ; unfold tm_subst ; rewrite !assoc ; rewrite hyperdoctrine_pair_comp_pr1' ; rewrite hyperdoctrine_pair_comp_pr2' ; rewrite <- p ; rewrite hyperdoctrine_pr1_comp ; rewrite hyperdoctrine_pr2_comp ; rewrite !id_right ; rewrite <- hyperdoctrine_pair_eta ; apply idpath). + abstract (rewrite hyperdoctrine_pair_comp_pr1' ; apply idpath). Defined.
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.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation.