I want to touch two points concerning Lawvere’s concept of Aufhebung:
Let us briefly recall the definition given in the entry. Given a topos define a level as an essential subtopos that is with fully faithful. This yields an adjoint modality via and . A level is higher iff
resolves if furthermore and is the Aufhebung (term taken from Hegel) of if every other level that resolves is higher than .
The first point which suggests that there might be something wrong here (at least in my understanding) is that this appears to imply that a quintessential localization aka quality type where is his own Aufhebung as then whence .
This is somewhat puzzling because Lawvere in (1991, p.10) asks for the Aufhebung of a level that is an quality type and also the Aufhebung operator computed in Kennett-Riehl-Roy-Zaks for some homotopical cats does have no fix points implying e.g. that sSet has no quintessential localizations. So there probably is a bug here!?
The second point is related to Mike’s quest in a recent thread to deconstruct the modalities internally. Taking a look at Urs’ table for differential cohesion and rearranging a bit :
This suggests to read the as Aufhebung with the left-peripheral just there to ensure that the Aufhebung exists at the preceding level so that we start with at the bottom, lift with carry-over , lift once more with final carry-over . As Aufhebung consists intuitively basically in shifting the ‘negative’ part to the ‘positive’ right at a higher level (in particular, the Aufhebung of a can be viewed as a stand-in for a left adjoint which transforms already at the same level) this could be viewed as a repeated rectification of - non-being. So the idea would be to put aside the base and the thickened topos and try to characterize the adjunctions in the table via the existence of the appropriate Aufhebungen. In order to find out whether this story holds water it would be necessary to check that the are indeed Aufhebungen and then that the carry-overs actually can be connected to these Aufhebungen, also the implicit quantification over all levels is potentially nasty from an internal point of view.