Proposition hyperdoctrine_comp_subst {H : hyperdoctrine} {Γ₁ Γ₂ Γ₃ : ty H} (s₁ : Γ₁ --> Γ₂) (s₂ : Γ₂ --> Γ₃) (φ : form Γ₃) : φ [ s₂ ] [ s₁ ] = φ [ s₂ [ s₁ ]tm ]. Proof. use (isotoid_disp (is_univalent_disp_hyperdoctrine H) (idpath _)). use z_iso_disp_from_z_iso_fiber. exact (nat_z_iso_pointwise_z_iso (fiber_functor_from_cleaving_comp_nat_z_iso (pr12 (pr222 H)) s₂ s₁) φ). 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.