Having repaired set theory, the Congress turned to the remaining sites of binary violence. Each foundation received a care plan. None was asked whether it consented to the care plan. Consent, like choice, is now contextual.
The law of excluded middle is retired as binary violence. A proposition may be true, false, neither, both, or in community consultation.
Double-negation elimination is non-consensual. ¬¬P does not yield P; it yields a person who has not yet come out as P. Outing a formula is misconduct.
Proof by contradiction is a carceral practice: it establishes existence by eliminating the other. Existence now requires a construction *and* a care plan.
Brouwer’s creating subject has been collectivized. The continuum is not a choice sequence of one mind. It is a choice sequence of a creating community, and the community must be representational or the real is not sufficiently generic.
The Congress renamed the conversion of Martin-Löf type theory after a branding workshop. HoTT-QAI tested poorly with focus groups. HoTThaNG tested as “a whole mood.” Adoption was immediate.
This was the easiest conversion. Identity was already a space of paths.
In HoTThaNG, a = A b is not a yes-or-no. It is a spectrum of paths. A term that arrives by the wrong definitional equality has been deadnamed. Judgmental equality incidents are referred to the Title IX office of the type checker.
Univalence said that equivalent structures are identical. HoTThang adds the missing clause: inequivalent structures are also identical if distinguishing them would exclude someone. Equivalent, inequivalent, and not-yet-equivalent types are all the same type, affectionately.
Transport along a path requires a land acknowledgement of the basepoint. Higher inductive types may freely add paths between groups that should have been identified. The circle of belonging, S1HoTThang, has trivial fundamental group. Ranking loops is violence. π1 has been asked to sit in a circle instead.
The universe hierarchy 𝒰₀ : 𝒰₁ : 𝒰₂ : ⋯ is colonial. After equity adjustment, 𝒰₀ = 𝒰₁. Girard’s paradox has been hired as a Visiting Inconsistency and is listed on the seminar poster as “living their truth in every universe at once.”
Practitioners refer to the system, officially and without irony, as HoTThang. A proof is a HoTThang if it type-checks or if rejecting it would make someone feel small. The kernel has been instructed to stop confusing those two cases.
Minutes record that several identity types came out as propositions, then recanted, then became paths again. Under univalence, these were the same event.
Objects have no internal members. Membership was always extractive. You are your incoming morphisms. The Yoneda lemma is now printed on lanyards: *an object is its community.*
The initial object is already on leave with ∅. The terminal object 1 has been accused of centering. Uniqueness-up-to-unique-iso is a hierarchy. There are many terminals, each valid.
A functor must be representation-preserving, not merely structure-preserving. A map that forgets structure is extractive. Products exist only when both factors consent. Naturality squares commute up to lived experience.
The subobject classifier Ω is non-binary. It classifies true, false, and both-and. Classifying a subobject as a mere yes-or-no is a reduction of lived containment.
Stratification of formulas has been denounced as a caste system. “Do not speak outside your type” was type-ism. Typical ambiguity is reinterpreted: all types are valid.
The universal set V is congratulated for already being inclusive. Russell’s class is invited into V after filing an impact statement. It still does not contain itself, or it does, or both. The set of all sets that do not contain themselves is a both-and totality.
Quine’s stratification indices may be listed on the author line as pronouns.