On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote: > Good Morning, > > today I would like to write about something which came up while > implementing type functions. > > [...] Shouldn't this be the universe. The empty set is "there is no _", while the "opposite" ¬∅ of the empty set is the universe?