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.
Equations
- Heyting.IsRegular a = (aᶜᶜ = a)
Equations
- Heyting.IsRegular.decidablePred x✝ = inst✝ x✝ᶜᶜ x✝
A Heyting algebra with regular excluded middle is a boolean algebra.
Equations
- One or more equations did not get rendered due to their size.
The boolean algebra of Heyting regular elements.
Equations
- Heyting.Regular α = { a : α // Heyting.IsRegular a }
The coercion Regular α → α
Equations
Equations
Equations
- Heyting.Regular.inf = { min := fun (a b : Heyting.Regular α) => ⟨↑a ⊓ ↑b, ⋯⟩ }
Equations
- Heyting.Regular.himp = { himp := fun (a b : Heyting.Regular α) => ⟨↑a ⇨ ↑b, ⋯⟩ }
Equations
- Heyting.Regular.hasCompl = { compl := fun (a : Heyting.Regular α) => ⟨(↑a)ᶜ, ⋯⟩ }
Equations
- Heyting.Regular.instInhabited = { default := ⊥ }
Equations
Regularization of a
. The smallest regular element greater than a
.
The Galois insertion between Regular.toRegular
and coe
.
Equations
- Heyting.Regular.gi = { choice := fun (a : α) (ha : ↑(Heyting.Regular.toRegular a) ≤ a) => ⟨a, ⋯⟩, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
A decidable proposition is intuitionistically Heyting-regular.