Heyting algebra morphisms #
A Heyting homomorphism between two Heyting algebras is a bounded lattice homomorphism that preserves Heyting implication.
We use the FunLike
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
HeytingHom
: Heyting homomorphisms.CoheytingHom
: Co-Heyting homomorphisms.BiheytingHom
: Bi-Heyting homomorphisms.
Typeclasses #
- toFun : α → β
- map_sup' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊔ b) = SupHom.toFun s.toSupHom a ⊔ SupHom.toFun s.toSupHom b
- map_inf' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊓ b) = SupHom.toFun s.toSupHom a ⊓ SupHom.toFun s.toSupHom b
- map_bot' : SupHom.toFun s.toSupHom ⊥ = ⊥
The proposition that a Heyting homomorphism preserves the bottom element.
- map_himp' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⇨ b) = SupHom.toFun s.toSupHom a ⇨ SupHom.toFun s.toSupHom b
The proposition that a Heyting homomorphism preserves the Heyting implication.
The type of Heyting homomorphisms from α
to β
. Bounded lattice homomorphisms that preserve
Heyting implication.
Instances For
- toFun : α → β
- map_sup' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊔ b) = SupHom.toFun s.toSupHom a ⊔ SupHom.toFun s.toSupHom b
- map_inf' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊓ b) = SupHom.toFun s.toSupHom a ⊓ SupHom.toFun s.toSupHom b
- map_top' : SupHom.toFun s.toSupHom ⊤ = ⊤
The proposition that a co-Heyting homomorphism preserves the top element.
- map_sdiff' : ∀ (a b : α), SupHom.toFun s.toSupHom (a \ b) = SupHom.toFun s.toSupHom a \ SupHom.toFun s.toSupHom b
The proposition that a co-Heyting homomorphism preserves the difference operation.
The type of co-Heyting homomorphisms from α
to β
. Bounded lattice homomorphisms that
preserve difference.
Instances For
- toFun : α → β
- map_sup' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊔ b) = SupHom.toFun s.toSupHom a ⊔ SupHom.toFun s.toSupHom b
- map_inf' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊓ b) = SupHom.toFun s.toSupHom a ⊓ SupHom.toFun s.toSupHom b
- map_himp' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⇨ b) = SupHom.toFun s.toSupHom a ⇨ SupHom.toFun s.toSupHom b
The proposition that a bi-Heyting homomorphism preserves the Heyting implication.
- map_sdiff' : ∀ (a b : α), SupHom.toFun s.toSupHom (a \ b) = SupHom.toFun s.toSupHom a \ SupHom.toFun s.toSupHom b
The proposition that a bi-Heyting homomorphism preserves the difference operation.
The type of bi-Heyting homomorphisms from α
to β
. Bounded lattice homomorphisms that
preserve Heyting implication and difference.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that a Heyting homomorphism preserves the bottom element.
The proposition that a Heyting homomorphism preserves the Heyting implication.
HeytingHomClass F α β
states that F
is a type of Heyting homomorphisms.
You should extend this class when you extend HeytingHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that a co-Heyting homomorphism preserves the top element.
The proposition that a co-Heyting homomorphism preserves the difference operation.
CoheytingHomClass F α β
states that F
is a type of co-Heyting homomorphisms.
You should extend this class when you extend CoheytingHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that a bi-Heyting homomorphism preserves the Heyting implication.
The proposition that a bi-Heyting homomorphism preserves the difference operation.
BiheytingHomClass F α β
states that F
is a type of bi-Heyting homomorphisms.
You should extend this class when you extend BiheytingHom
.
Instances
This can't be an instance because of typeclass loops.
Instances For
Copy of a HeytingHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
id
as a HeytingHom
.
Instances For
Composition of HeytingHom
s as a HeytingHom
.
Instances For
Copy of a CoheytingHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
id
as a CoheytingHom
.
Instances For
Composition of CoheytingHom
s as a CoheytingHom
.
Instances For
Copy of a BiheytingHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
id
as a BiheytingHom
.
Instances For
Composition of BiheytingHom
s as a BiheytingHom
.