We envision this section to allow the exploration of proofs directly via the constructions involved in them: highlight particular parts of the dual structures which arise, highlight specific transformations happening to them during the arguments, etc.