set_theory.idr

module Main

infix 5 /\, \/

(/\) : Type -> Type -> Type
(/\) a b = (a, b)

(\/) : Type -> Type -> Type
(\/) a b = Either a b

Exist : (a -> Type) -> Type
Exist f = (a ** f a)

NotExist : (a -> Type) -> Type
NotExist = Not . Exist

Forall : (a -> Type) -> Type
Forall {a} f = (x : a) -> f x

Set : Type -> Type
Set a = a -> Type

member : a -> Set a -> Type
member x s = s x

notMember : a -> Set a -> Type
notMember x s = Not (x `member` s)

subset : Set a -> Set a -> Type
subset {a} s1 s2 = (x : a) -> x `member` s1 -> x `member` s2

equiv : Set a -> Set a -> Type
equiv s1 s2 = (s1 `subset` s2) /\ (s2 `subset` s1)

map : (a -> b) -> (Set a -> Set b)
map f s = \b => Exist $ \a => (a `member` s) /\ (f a = b)

insert : a -> Set a -> Set a
insert x s = \y => (x = y) \/ (y `member` s)

remove : a -> Set a -> Set a
remove x s = \y => (Not (x = y)) /\ (y `member` s)

empty : Set a
empty = \y => Void

union : Set a -> Set a -> Set a
union s1 s2 = \x => (x `member` s1) \/ (x `member` s2)

intersection : Set a -> Set a -> Set a
intersection s1 s2 = \x => (x `member` s1) /\ (x `member` s2)

disjointUnion : Set a -> Set b -> Set (Either a b)
disjointUnion s1 s2 = (map Left s1) `union` (map Right s2)

join : Set (Set a) -> Set a
join ss = \x => Exist (\s => (x `member` s) /\ (s `member` ss))

bind : (a -> Set b) -> (Set a -> Set b)
bind f = join . map f

prod : Set a -> Set b -> Set (a, b)
prod s1 s2 = \(x, y) => (x `member` s1) /\ (y `member` s2)

fun : Set a -> Set b -> Set (a -> b)
fun s1 s2 = \f => Forall (\x => x `member` s1 -> f x `member` s2)

evenNats : Set Nat
evenNats = \x => x `mod` 2 = 0

noElementsInZero1 : Forall (\x => x `notMember` Main.empty)
noElementsInZero1 x p = p

noElementsInZero2 : NotExist (\x => x `member` Main.empty)
noElementsInZero2 (x ** p) = p

indempotentUnion : (s : Set a) -> (s `union` s) `equiv` s
indempotentUnion s = (\x => either id id, \x => Left)

emptyIsUnitForUnion : (s : Set a) -> (s `union` Main.empty) `equiv` s
emptyIsUnitForUnion s = (\x => either id void, \x => Left)

emptyIsZeroForIntersection : (s : Set a) -> (s `intersection` Main.empty) `equiv` Main.empty
emptyIsZeroForIntersection s = (\x => snd, \x => void)


-- sigma : (f : Set a -> Type) -> Type
-- sigma f = Set (x : Set a ** f x)

-- Groupoid : Type -> Type
-- Groupoid a = sigma (\M : Set a => (M `prod` M) `fun` M)