Let us say a GL-category \footnote{so named for reasons to be explained later} is a structure <L, L’, F, F’> (which, in typical abuse of language, we may sometimes identify with simply the name of L) of the following sort:

A) A lexcategory L

A’) A lexcategory L’ internal to L

B) A lexfunctor F from L to Glob(L’) \footnote{Presentational TODO: it will be useful at some point to specify a convention that a functor from an actual category to an internal category always means a functor from the former to the globalization of the latter; once establishing this convention, we can drop the distracting explicit “Glob”s of the sort here.

In a similar vein, it will also be useful to explicitly establish the convention that a lexfunctor H : C \to D can also be implicitly regarded as a homomorphism : Glob(C’) \to Glob(H[C’]) for any structure C’ internal to C in the natural way}

B’) A lexfunctor F’ from L’ to F[L’] internal to L

C) Such that F(F(x)) = F'(F(x)) for any object/morphism x in L, construed appropriately (I’m writing with some abuse of notation (see previous footnote), but this condition is similar to the third condition in the description of introspective theory homomorphisms)

C’) Such that, in the internal logic of L, we have that F'(F'(x)) = F[F’](F'(x)) for any object/morphism x in F[L’]

Note that the theory of GL-categories is essentially algebraic and can thus be identified with a lexcategory (the generic lexcategory with an internal GL-category), which for now let us call TheoryGL.

In the standard way as for any essentially algebraic theory, we also get a notion of GL-category homomorphism; a GL-category homomorphism between GL-categories <L_1, L_1′, F_1, F_1′> and <L_2, L_2′, F_2, F_2′> is

- A lex functor H : L_1 \to L_2
- Such that H[L_1′] = L_2′
- Such that H[F_1(x)] = F_2(H(x)) for any object/morphism x in L_1, where the H on the left acts as a functor from Glob(L_1′) to Glob(H[L_1′]) = Glob(L_2′) in the natural fashion
- Such that H[F_1′] = F_2′

Now observe that TheoryGL (the generic lexcategory with an internal GL-category) can be equipped as an introspective theory <TheoryGL, L, S, Q> as follows:

- TheoryGL is the generic lexcategory with an internal GL-category <L, L’, F, F’>.
- L, thus, is the underlying lexcategory of that internal GL-category.
- To specify S now is, by the nature of TheoryGL and of S as a lexfunctor from TheoryGL to Glob(L), to specify an L-internal GL-category; specifically, we will take S to correspond to the L-internal GL-category <L’, F[L’], F’, F[F’]>. Note that this choice is indeed a GL-category, with structure/conditions A, B, and C in such S corresponding to structure/conditions A’, B’, and C’ in <L, L’, F, F’>, and further structure/conditions A’, B’, and C’ in S obtained by application of F to the former, respectively. [TODO: Though this is indeed a complete description of what is going on here, this language may be clunky… Perhaps reword in some fashion]
- Finally, to specify Q is to specify a GL-category homomorphism from our generic GL-category <L, L’, F, F’> to the globalization (within TheoryGL) of the L-internal GL-category S = <L’, F[L’], F’, F[F’]>. For this, we take the underlying lexfunctor of that homomorphism to be F. Verifying that F is indeed a GL-category homomorphism requires verifying three further conditions (as in the bulleted list above), which in this case come out to F[L’] = F[L’] (trivially true), F(F(x)) = F'(F(x)) interpreted suitably (true by condition C for L as a GL-category), and F[F’] = F[F’] (again, trivially true).

This completes the definition of <TheoryGL, L, S, Q> and demonstration of it as an introspective theory.

Next, I intend to show that this is in fact the initial introspective theory; that is, that it has a unique introspective theory homomorphism into any other introspective theory <T, T’, S_2, Q_2>. [TODO: I really need to learn how to pick better names for variables…]

Such a homomorphism amounts to a lexfunctor H from TheoryGL to T satisfying certain conditions (specifically, that H[L] = T’ and that the identity H(S(x)) = S_2(H(x)) holds, suitably interpreted), which is to say (by the nature of TheoryGL) such a homomorphism amounts to a T-internal GL-category <T’, . [TODO: Finish]

[TODO: Discuss more generally the free introspective theory extending a given essentially algebraic theory extending the theory of lexcategories, given in essentially the same manner (replacing lexcat with whatever, lexfunc with whatever-homomorphism), giving rise to GL-(whatevers) (e.g., GL-toposes, GL-(lex)categories with coproducts, etc.)]

Finally, let us show that given any introspective theory <T, T’, S, Q>, we have that T can be interpreted as a GL-category as well; specifically, we will have a GL-category <T, T’, S, Q interpreted suitably> [TODO: Finish]