Plato's Sophist and Type Theory (older post)

Suppose we had a type $A \rightarrow B$. Then application $a : A, f : A\rightarrow B \vdash f a : B$ can be 'internalized' as a type \[ A\rightarrow (A\rightarrow B) \rightarrow B \] But application of this type can likewise be internalised as\[ A \rightarrow (A \rightarrow B) \rightarrow (A\rightarrow (A\rightarrow B) \rightarrow B ) \rightarrow B \] and so forth. This is similar to the 'third man' argument of the Parmenides. Take $B$ to be the 'truth-value' type $\Omega$. The 'canopy' argument in fact seems to herald the idea that a type (i.e. a 'form' or 'unsaturated' propositional function) should be seen not only a 'set' but as a 'space' as in homotopy type theory. In a passage of the Sophist 237 there is a remarkable discussion on 'non-being'. You cannot talk about non-being because by doing so you already attribute it implicitly the mark of a something, an ought - both unity and being. Now this passage is in many ways an anticipation of the rule of contradiction (for $\bot$) in natural deduction as well as its logical deployment in axiomatic set theory, specially dealing with $\emptyset$ in formal proofs. But most interesting is the connection to Martin-Löf type theory: the zero type or empty type $\mathbb{O}$. This type is not inhabited by anything. But yet to use this type, to reason with it, you must assume that it is inhabited $ a : \mathbb{O}$.  Martin-Löf type theory allows us to flesh out Plato's intuition about the connection between falsehood, nothingness and absurdity. The empty set is a paradigm of the initial object of a category. There is a unique set theoretic function $f : \emptyset \rightarrow X$ for a given set $X$. Correspondingly the type $\mathbb{O}\rightarrow A$ is inhabited where $A$ is for example some non-empty inductive type. Thus we can speak meaningfully about nothing. Consider the very difficult passage Sophist 243-246 that clearly picks up on and rectifies the Parmenides. But for Plato what are 'Being', 'Unity' and the 'Whole' ?  We can consider the unit type $\mathbb{I}$ as corresponding to 'Unity' and think of it as either a set-theoretic singleton $\{u\}$ or as a contractible type where equality is interpreted as a homotopy path. In this sense it is a homogenous space much like the 'sphere' in Parmenides' poem. Plato does indeed distinguish between pure unity and a whole participating of unity. The singleton set is a paradigm of a terminal object in a category.
The 'Whole' is clearly a 'universe' type $U$ or $Type$.  It is a difficult problem to relate the 'Whole' to 'Unity'. What does it mean even for the 'Whole' to participate of 'Unity' ? That there is one supreme universe $Unity$ with only one inhabitant $Type : Unity$ ? But then we could not have accumulativity : $ a : Type$ implying that $ a : Unity$. Or, categorically, how do we interpret that all objects $A$ admit a unique morphism $A \rightarrow 1$ ? Category theoretically a ($\infty-\enspace$) groupoid is a candidate for a category 'participating in unity'. There is a tension between unital being $\mathbb{I}$ and the being-whole, the being spread out and shared by all beings $Type$. The logic in this passage is apparently 'type-free' and impredicative. 'Being' $: \Pi ( X: Type), \Omega$ and 'Unity': $\Pi (X : Type), \Omega$ seem to be able to be applied meaningfully to anything (indeed $Type : Type$). The passages on 'names' and 'reference' is quite striking. Specially when Plato conjures up 'names that refer to names' and a name referring only to itself (imagine a type only inhabited by itself). Part of Plato's argument is that no matter what in reality 'is' the fact is that there is a plurality of \names. In the later section on the five suprema genera we may ask: why is there not also a form for 'participation' itself ?What are some fundamental kinds of types ? The empty type $\mathbb{O}$, the unit type $\mathbb{I}$, the universe(s)  $\mathcal{U} $ (or $Type_i$), equality $ \Pi ( X\enspace Y: Type), Prop $, number $Nat : Type$ and the interval $\mathbf{I}$ for path spaces or cubical sets in homotopy type theory. Paths represent change, the interval represents temporality. Plato speaks of equality being or not being equal to something, just as Voevodsky speaks of equality being equivalent to equivalence.