Latte-sets 1.0b10-SNAPSHOT

Released under the MIT Licence

A formalization of (typed) Set theory in LaTTe.

Installation

To install, add the following dependency to your project or build file:

[latte-sets "1.0b10-SNAPSHOT"]

Namespaces

latte-sets.algebra

The boolean algebra operators for sets.

latte-sets.equiv

Equivalence relations

latte-sets.pfun

Partial functions are defined in this namespace as relations (in the type theoretic sense) of type (==> T U :type) together with a domain dom of type (set T) and a codomain cod of type (set U) such that for any element of the domain there is a unique image in the codomain.

latte-sets.powerrel

Notions about the relational powerset construction.

latte-sets.powerset

Notions about the powerset construction.

latte-sets.quant

Quantifiers over sets (rather than types), with most definitions specialized from latte-prelude.quant.

latte-sets.ralgebra

The relation algebra operators.

latte-sets.rel

A relation from elements of a given type T to elements of U is formalized with type (==> T U :type).

latte-sets.set

Set-theoretic notions based on the subset approach of type theory.