# @hackage/type-settheory0.1.3.1

Sets and functions-as-relations in the type system

### Categories

### License

BSD-3-Clause

### Maintainer

daniels@community.haskell.org

### Links

### Versions

Type classes can express sets and functions on the type level, but they are not first-class. This package expresses type-level sets and functions as *types* instead.

Instances are replaced by value-level proofs which can be directly manipulated; this makes quite a bit of (constructive) set theory expressible; for example, we have:

Subsets and extensional set equality

Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a sort of dependent sum and product

Functions and their composition, images, preimages, injectivity

The proposition-types (derived from the `:=:`

equality type) aren't meaningful purely by convention; they relate to the rest of Haskell as follows: A proof of `A :=: B`

gives us a safe coercion operator `A -> B`

(while the logic is inevitably inconsistent *at compile-time* since `undefined`

proves anything, I think that we still have the property that if the `Refl`

value is successfully pattern-matched, then the two parameters in its type are actually equal).

### Installation

### Dependencies (6)

### Dependents (1)

@hackage/acme-everything