Copyright | (C) 2019 Oleg Grenrus |
---|---|
License | BSD-3-Clause (see the file LICENSE) |
Maintainer | Oleg Grenrus <oleg.grenrus@iki.fi> |
Safe Haskell | Safe |
Language | Haskell2010 |
Algebra.Heyting
Description
Synopsis
- class BoundedLattice a => Heyting a where
Documentation
class BoundedLattice a => Heyting a where Source #
A Heyting algebra is a bounded lattice equipped with a binary operation \(a \to b\) of implication.
Laws
x==>
x ≡top
x/\
(x==>
y) ≡ x/\
y y/\
(x==>
y) ≡ y x==>
(y/\
z) ≡ (x==>
y)/\
(x==>
z)
Minimal complete definition
Instances
Heyting Bool Source # | |
Heyting () Source # | |
Heyting All Source # | |
Heyting Any Source # | |
Heyting ZeroHalfOne Source # | |
Defined in Algebra.Lattice.ZeroHalfOne Methods (==>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne Source # neg :: ZeroHalfOne -> ZeroHalfOne Source # (<=>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne Source # | |
Heyting M2 Source # | |
Heyting a => Heyting (Identity a) Source # | |
Heyting a => Heyting (Endo a) Source # | |
(Ord a, Finite a) => Heyting (Set a) Source # | |
(Eq a, Hashable a, Finite a) => Heyting (HashSet a) Source # | |
(Ord a, Bounded a) => Heyting (Ordered a) Source # | This is interesting logic, as it satisfies both de Morgan laws; but isn't Boolean: i.e. law of exluded middle doesn't hold. |
Heyting (Free a) Source # | |
Heyting a => Heyting (b -> a) Source # | |
Heyting (Proxy a) Source # | |
Heyting a => Heyting (Const a b) Source # | |
Heyting a => Heyting (Tagged b a) Source # | |