Definition make_univalent_hyperdoctrine (C : category) (D : disp_cat C) (T : Terminal C) (BP : BinProducts C) (HD : cleaving D) (HD' : locally_propositional D) (HD'' : is_univalent_disp D) (HC : is_univalent C) : univalent_hyperdoctrine := C ,, D ,, T ,, BP ,, HD ,, HD' ,, HD'' ,, HC. Coercion hyperdoctrine_to_preorder_hyperdoctrine (H : hyperdoctrine) : preorder_hyperdoctrine. Proof. exact (pr1 H ,, pr12 H ,, pr122 H ,, pr1 (pr222 H) ,, pr12 (pr222 H) ,, pr122 (pr222 H)). 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.