@olivia what's striking about this characterization: "in making available what we are already acquainted with", my pov in type theory disposes me to consider that just this capacity to "make available", while not identical to, has a nontrivial relationship to the nature of what we think of as truth or mathematical structure. i find her formulation apt because she does not foreclose this, but also bc she insists that in the achievement of any result we only encounter ourselves, and she is right