Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The compact ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.
We introduce Heraclitean Dialectical Concept Spaces (HDCS), a topological framework for modelling stagewise structural change in systems of concepts. A stage consists of a nonempty concept set, a feasible family generating an external topology, and a neighbourhood assignment carrying additional relational structure. Neighbourhood overlap induces adjacency and channel ideals. Candidate emergence is represented by the CCER construction: an interaction profile, finite admissible cores, and anchored witnesses determine nonempty open candidate regions in uncovered remainder structure. Selected candidates may be reified as new atomic concepts at a later stage, while partial injective carry maps separately track persistence of existing identities. The resulting history space is obtained as a quotient of the disjoint union of stage spaces with the corresponding final topology. Product concept spaces extend the construction to cross-domain interaction. We derive support characterizations, mediated-interaction components, canonical CCER envelopes, monotonicity and impossibility criteria, product-space factorization, and invariance under concept-space isomorphism. Applications to monetary transformation, zero and representation, mammalian middle-ear evolution, and AI-related labour change illustrate the framework. HDCS is intended as a structural formalism rather than a causal or predictive theory of historical change.
We study the computational complexity of finding fixed points of set-valued contractions. We first formulate a computational problem for Nadler's fixed-point theorem, PROJECTED-NADLER, and prove that it is CLS-complete by showing its equivalence to CONTINUOUS-LOCALOPT. We then establish a stronger converse to Nadler's theorem, which can be applied as a tool to analyze the convergence rate of the set-valued basic iteration procedure. Finally, we reduce the large-margin triplet stationarity problem to PROJECTED-NADLER. Combining the argument for CLS-hardness of exact triplet stationarity problem [Yan et al. 2025] with the CLS-hardness of approximate KKT points of quadratic programs [Fearnley et al. 2025], we obtain CLS-completeness of large-margin triplet stationarity at any prescribed accuracy.