Heyting regular elements #
This file defines Heyting regular elements, elements of a Heyting algebra that are their own double complement, and proves that they form a boolean algebra.
From a logic standpoint, this means that we can perform classical logic within intuitionistic logic by simply double-negating all propositions. This is practical for synthetic computability theory.
Main declarations #
IsRegular
:a
is Heyting-regular ifaᶜᶜ = a
.Regular
: The subtype of Heyting-regular elements.Regular.BooleanAlgebra
: Heyting-regular elements form a boolean algebra.
References #
- [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]
An element of a Heyting algebra is regular if its double complement is itself.
Instances For
A Heyting algebra with regular excluded middle is a boolean algebra.
Instances For
The boolean algebra of Heyting regular elements.
Instances For
The coercion Regular α → α
Instances For
Regularization of a
. The smallest regular element greater than a
.
Instances For
The Galois insertion between Regular.toRegular
and coe
.
Instances For
A decidable proposition is intuitionistically Heyting-regular.