Proposition to_disp_mor_hyperdoctrine {H : preorder_hyperdoctrine} {Γ₁ Γ₂ : ty H} {Δ : form Γ₁} {φ : form Γ₂} (s : tm Γ₁ Γ₂) (p : Δ ⊢ φ [ s ]) : Δ -->[ s ] φ. Proof. refine (transportf (λ z, _ -->[ z ] _) (id_left _) (p ;; _)%mor_disp). exact (mor_disp_of_cartesian_lift _ _ (hyperdoctrine_cleaving H _ _ 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.