Definition cha_basis_rel {H : complete_heyting_algebra} {B : cha_basis_data H} (b₁ b₂ : B) : hProp := pr22 B b₁ b₂.
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.