init component

node_modules/fp-ts/lib/HeytingAlgebra.d.ts

@@ -0,0 +1,32 @@
+/**
+ * Heyting algebras are bounded (distributive) lattices that are also equipped with an additional binary operation
+ * `implies` (also written as `→`). Heyting algebras also define a complement operation `not` (sometimes written as
+ * `¬a`)
+ *
+ * However, in Heyting algebras this operation is only a pseudo-complement, since Heyting algebras do not necessarily
+ * provide the law of the excluded middle. This means that there is no guarantee that `a ∨ ¬a = 1`.
+ *
+ * Heyting algebras model intuitionistic logic. For a model of classical logic, see the boolean algebra type class
+ * implemented as `BooleanAlgebra`.
+ *
+ * A `HeytingAlgebra` must satisfy the following laws in addition to `BoundedDistributiveLattice` laws:
+ *
+ * - Implication:
+ *   - `a → a <-> 1`
+ *   - `a ∧ (a → b) <-> a ∧ b`
+ *   - `b ∧ (a → b) <-> b`
+ *   - `a → (b ∧ c) <-> (a → b) ∧ (a → c)`
+ * - Complemented
+ *   - `¬a <-> a → 0`
+ *
+ * @since 2.0.0
+ */
+import { BoundedDistributiveLattice } from './BoundedDistributiveLattice'
+/**
+ * @category model
+ * @since 2.0.0
+ */
+export interface HeytingAlgebra<A> extends BoundedDistributiveLattice<A> {
+  readonly implies: (x: A, y: A) => A
+  readonly not: (x: A) => A
+}