Convert set to sealed interface.

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/structures/Magma.java

@@ -2,7 +2,7 @@
 
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Element;
-import com.github.vincentk.dedekind.sets.Set;
+import com.github.vincentk.dedekind.sets.NonEmptySet;
 import com.github.vincentk.dedekind.sets.binary.function.arithmetic.Addition;
 import com.github.vincentk.dedekind.sets.binary.function.arithmetic.Multiplication;
 import com.github.vincentk.dedekind.sets.binary.function.operation.BinaryOperation;
@@ -22,7 +22,7 @@ public interface Magma<
 C extends Cardinality,
 T extends Magma<E, C, T>>
 extends
-Set<E, C, T>
+NonEmptySet<E, C, T>
 {
     interface Oe<E extends Oe<E>>
     extends

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Family.java

@@ -2,6 +2,7 @@
 
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Element;
+import com.github.vincentk.dedekind.sets.NonEmptySet;
 import com.github.vincentk.dedekind.sets.Set;
 
 /**
@@ -22,7 +23,7 @@ public interface Family<
 P extends Pair<De, Re, P>,
 Z extends Family<De, C, D, Re, P, Z>
 >
-extends Set<P, C, Z>
+extends NonEmptySet<P, C, Z>
 {
     /**
      * @return the image of the function.

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Net.java

@@ -2,7 +2,7 @@
 
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Element;
-import com.github.vincentk.dedekind.sets.ordered.Directed;
+import com.github.vincentk.dedekind.sets.ordered.DirectedSet;
 
 /**
  * @see https://en.wikipedia.org/wiki/Net_(mathematics)
@@ -11,20 +11,20 @@
 public interface Net<
 
 // Domain of the net and its elements:
-E extends Directed.De<E>,
+E extends DirectedSet.De<E>,
 C extends Cardinality,
-D extends Directed<E, C, D>,
+D extends DirectedSet<E, C, D>,
 
 // Range of the net:
 T extends Element<T>,
 
 
 //Implementation details:
-P extends Pair<E, T, P> & Directed.De<P>,
+P extends Pair<E, T, P> & DirectedSet.De<P>,
 Z extends Net<E, C, D, T, P, Z>
 >
 extends
 Family<E, C, D, T, P, Z>,
-Directed<P, C, Z>
+DirectedSet<P, C, Z>
 {
 }

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/TopologicalSpace.java

@@ -3,7 +3,7 @@
 
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Element;
-import com.github.vincentk.dedekind.sets.Set;
+import com.github.vincentk.dedekind.sets.NonEmptySet;
 
 /**
  * @see https://en.wikipedia.org/wiki/Topological_space
@@ -17,7 +17,7 @@ public interface TopologicalSpace<
 M extends TopologicalSpace<E, C, M>
 >
 extends
-Set<E, C, M>
+NonEmptySet<E, C, M>
 {
     interface Me<
     E extends Me<E>

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/CountableSet.java

@@ -13,7 +13,7 @@ public interface CountableSet<
 T extends CountableSet<E, C, T>
 >
 extends
-Set<E, C, T>
+NonEmptySet<E, C, T>
 {
     /**
      * A set is countable exactly if its elements can be arranged in a {@link Sequence}

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/EmptySet.java

@@ -13,6 +13,7 @@
  */
 public final class EmptySet<E extends Element<E>>
 implements
+Set<E, Empty, EmptySet<E>>,
 Empty,
 FiniteSet.B64<E, Empty, EmptySet<E>>
 {

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/NonEmptySet.java

@@ -1,5 +1,6 @@
 package com.github.vincentk.dedekind.sets;
 
+non-sealed
 public interface NonEmptySet<
 E extends Element<E>,
 C extends Cardinality,
@@ -11,4 +12,22 @@ public interface NonEmptySet<
     default boolean isEmpty() {
 	return false;
     }
+
+    /**
+     * @param that
+     * @return this &cup; that
+     */
+    @Override
+    default Set<E, ?, ?> union(Set<E, ?, ?> that) {
+
+	if (isEmpty()) return that;
+	if (that.isEmpty()) return this;
+
+	final var cpl = complement(that);
+	if (cpl.isEmpty()) return that;
+
+	// TODO: the cardinality of the union is actually not known
+	// at this point:
+	return new Union<E, C>((NonEmptySet<E, ?, ?>) cpl, (NonEmptySet<E, ?, ?>) that);
+    }
 }

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/Set.java

@@ -12,14 +12,16 @@
  * 
  * @see https://en.wikipedia.org/wiki/Set_(mathematics)
  */
-public
+@SuppressWarnings("rawtypes") // Permits clause does not expect generic type arguments.
+sealed public
 interface Set<
 E extends Element<E>,
 C extends Cardinality,
 T extends Set<E, C, T>>
 extends
 Identity<Set<E, ?, ?>>,
 Element<Set<E, ?, ?>>
+permits EmptySet, NonEmptySet
 {
     @Override
     default boolean eq(Set<E, ?, ?> that) {
@@ -42,29 +44,19 @@ default boolean contains(E elem) {
     default boolean isEmpty() {
 	return this instanceof EmptySet<?>;
     }
-
+    
     /**
      * @param that
-     * @return this &cap; that
+     * @return this &cup; that
      */
-    default Set<E, ?, ?> intersection(Set<E, ?, ?> that) {
-	return where(x -> that.contains(x));
-    }
+    Set<E, ?, ?> union(Set<E, ?, ?> that);
 
     /**
      * @param that
-     * @return this &cup; that
+     * @return this &cap; that
      */
-    default Set<E, ?, ?> union(Set<E, ?, ?> that) {
-
-	if (isEmpty()) return that;
-
-	if (that.isEmpty()) return this;
-
-	final var cpl = complement(that);
-	if (cpl.isEmpty()) return that;
-
-	return new Union<E, C>(this, cpl);
+    default Set<E, ?, ?> intersection(Set<E, ?, ?> that) {
+	return where(x -> that.contains(x));
     }
 
     /**
@@ -100,7 +92,7 @@ default boolean sub(Set<E, ?, ?> that) {
     default boolean sup(Set<E, ?, ?> that) {
 	return that.complement(this).isEmpty();
     }
-    
+
     /**
      * Apply a function to every element &isin; this.
      * 

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/SingletonSet.java

@@ -16,7 +16,12 @@ public interface SingletonSet<E extends Element<E>, S extends SingletonSet<E, S>
 FiniteSet.B64<E, Small.One, S>
 {
     E elem();
-
+
+    @Override
+    default boolean contains(E that) {
+	return elem().eq(that);
+    }
+
     @Override
     default Set<E, ? extends Small.One, ?> where(Predicate<E> Φ) {
 	return Φ.test(elem()) ? this : EmptySet.empty();

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/Union.java

@@ -9,12 +9,28 @@ record Union<
 E extends Element<E>,
 C extends Cardinality
 >
-(Set<E, ?, ?> fst, Set<E, ?, ?> snd)
+(NonEmptySet<E, ?, ?> fst, NonEmptySet<E, ?, ?> snd)
 implements
 NonEmptySet<E, C, Union<E, C>>
 {
     @Override
-    public Set<E, ?, ?> where(Predicate<E> Φ) {
-	return fst().where(Φ).union(snd().where(Φ));
+    public boolean
+    contains(E elem) {
+	return fst().contains(elem) || snd().contains(elem);
     }
-}
+
+    @Override
+    public
+    Set<E, ?, ?>
+    where(Predicate<E> Φ)
+    {
+
+	final var w1 = fst().where(Φ);
+	final var w2 = snd().where(Φ);
+
+	if (w1.isEmpty()) return w2;
+	if (w2.isEmpty()) return w1;
+
+	return fst().where(Φ).union(w2);
+    }
+}

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/binary/function/operation/Closure.java

@@ -2,6 +2,7 @@
 
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Element;
+import com.github.vincentk.dedekind.sets.NonEmptySet;
 import com.github.vincentk.dedekind.sets.Set;
 
 /**
@@ -39,7 +40,7 @@ public interface Closure<
 // Implementing class:
 T extends Set<E, C, T> & Closure<C, E, A, F, B, T>
 >
-extends Set<E, C, T>, BinaryOperation<F, T>
+extends NonEmptySet<E, C, T>, BinaryOperation<F, T>
 {
     // Enable to force a type check:
     B ap(B a);

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/ordered/Directed.java → dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/ordered/DirectedSet.java

@@ -15,10 +15,10 @@
  * 
  * @see https://en.wikipedia.org/wiki/Directed_set
  */
-public interface Directed<
-E extends Directed.De<E>,
+public interface DirectedSet<
+E extends DirectedSet.De<E>,
 C extends Cardinality,
-T extends Directed<E, C, T>
+T extends DirectedSet<E, C, T>
 >
 extends NonEmptySet<E, C, T> {
 

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/ordered/Lattice.java

@@ -22,7 +22,7 @@ public interface Lattice<
 
     interface Le<E extends Le<E>>
     extends
-    SemiLattice.Join.Je<E>, SemiLattice.Meet.Me<E>, Directed.De<E>
+    SemiLattice.Join.Je<E>, SemiLattice.Meet.Me<E>, DirectedSet.De<E>
     {	
 
     }

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/ordered/PoSet.java

@@ -2,7 +2,7 @@
 
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Element;
-import com.github.vincentk.dedekind.sets.Set;
+import com.github.vincentk.dedekind.sets.NonEmptySet;
 import com.github.vincentk.dedekind.sets.binary.relation.homogeneous.PartialOrder;
 
 /**
@@ -18,7 +18,7 @@ public interface PoSet<
 C extends Cardinality,
 T extends PoSet<E, C, T>
 >
-extends Set<E, C, T>
+extends NonEmptySet<E, C, T>
 {
     interface Pe<E extends Pe<E>>
     extends

dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/ordered/SemiLattice.java

@@ -35,7 +35,7 @@ interface Join<
     >
     extends
     SemiLattice<E, C, T>,
-    Directed<E, C, T>
+    DirectedSet<E, C, T>
     {
 	interface Je<E extends Je<E>>
 	extends

dedekind-ontology/src/test/java/com/github/vincentk/dedekind/sets/UnionTest.java

@@ -0,0 +1,29 @@
+package com.github.vincentk.dedekind.sets;
+
+import static org.assertj.core.api.Assertions.assertThat;
+
+import org.junit.jupiter.api.Test;
+
+import com.github.vincentk.dedekind.algebra.numbers.N;
+
+public class UnionTest {
+
+    private static final SingletonSet<N.N63.Ne, ?> S1 = new SingletonSet.Ordered.Default<>(N.ONE);
+    private static final SingletonSet<N.N63.Ne, ?> S2 = new SingletonSet.Ordered.Default<>(N.TWO);
+    private static final EmptySet<N.N63.Ne> EMPTY = EmptySet.empty();
+
+    @Test
+    public void testConstruction() {
+	assertThat(EMPTY.union(EMPTY)).isEqualTo(EMPTY);
+	assertThat(S1.union(EMPTY)).isEqualTo(S1);
+	assertThat(EMPTY.union(S1)).isEqualTo(S1);
+	assertThat(S1.union(S1)).isEqualTo(S1);
+
+	final var u2 = S1.union(S2);
+	assertThat(u2).isInstanceOf(Union.class);
+	assertThat(u2.contains(N.ONE)).isTrue();
+	assertThat(u2.contains(N.TWO)).isTrue();
+
+	assertThat(u2.where(x -> x.eq(N.ZERO))).isEqualTo(EMPTY);
+    }
+}