Definition cha_basis_laws {H : complete_heyting_algebra} (B : cha_basis_data H) : UU := (∏ (b₁ b₂ b₃ : B), cha_basis_rel b₁ b₂ → cha_basis_rel b₂ b₃ → cha_basis_rel b₁ b₃) × (∏ (x : H), x = \/_{ i : ∑ (b : B), cha_basis_incl b ≤ x } cha_basis_incl (pr1 i)) × (∏ (b₁ b₂ : B), cha_basis_rel b₁ b₂ → cha_basis_incl b₂ ≤ cha_basis_incl 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.