Proposition hyperdoctrine_id_subst {H : hyperdoctrine} {Γ : ty H} (φ : form Γ) : φ [ tm_var _ ] = φ. Proof. refine (!_). use (isotoid_disp (is_univalent_disp_hyperdoctrine H) (idpath _)). use z_iso_disp_from_z_iso_fiber. exact (_ ,, is_nat_z_iso_fiber_functor_from_cleaving_identity (pr12 (pr222 H)) Γ φ). 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.