Proposition hyperdoctrine_formula_eq {H : hyperdoctrine} {A : ty H} {φ ψ : form A} (p : φ ⊢ ψ) (q : ψ ⊢ φ) : φ = ψ. Proof. use (isotoid_disp (is_univalent_disp_hyperdoctrine H) (idpath _)). use make_z_iso_disp. - exact p. - refine (q ,, _ ,, _) ; apply (pr122 (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.