Definition make_complete_heyting_algebra (X : hSet) (L : bounded_lattice X) (CL : is_complete_lattice L) (EL : exponential L) : complete_heyting_algebra := X ,, L ,, CL ,, EL. Coercion complete_heyting_algebra_to_carrier (H : complete_heyting_algebra) : hSet. Proof. exact (pr1 H). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting.