Proper classes (in the project's sense: circular self-embedding structures) have their mathematical home in terminal coalgebras νF ≅ F(νF).
Logic
The discipline entrances are dictionary-level correspondences: a ladder built in the other party's language, withdrawn once climbed.
Under the Anti-Foundation Axiom, every (flat) system of equations has a unique solution (Aczel's Solution Lemma); primordial equations replace axiomatic propositions on this basis.
Bisimulation serves as the identity criterion; in the finite case it is decidable via Paige–Tarjan partition refinement.
The rotor sequent calculus RSC₀ is sound and complete.
Generation-preserving ↔ truth-preserving: dictionary correspondence between the inference norms of generative and classical logic.