A Heyting algebra is a bounded lattice equipped with a binary operation of relative pseudo-complementation (implication). It is the algebraic semantics of intuitionistic (constructive) logic — a logic where the law of excluded middle does not necessarily hold, and proofs of existence must provide a witness.
Formally, a Heyting algebra is a partially ordered set (H, ≤) that is a bounded lattice (has meets ∧, joins ∨, top ⊤, and bottom ⊥) with an additional operation → satisfying: c ≤ (a → b) if and only if (c ∧ a) ≤ b. This condition — residuation — makes → the right adjoint to ∧.
Every Boolean algebra is a Heyting algebra, but not every Heyting algebra is Boolean. The difference is the law of excluded middle: in a Boolean algebra, a ∨ ¬a = ⊤ for all a; in a Heyting algebra, this may fail.
For a curriculum introduction, see the existing learn-heyting-algebras skill. For how the relationality derivation produces a Heyting algebra from the relations among judgements, see Relational Heyting Algebra in the relationality discipline.