If you want to be clear about the quantifier alternation in a theorem represented by a categorical diagram, consider it to be built stepwise, where even steps are universal and odd steps existential.
Minimally write step number labels on things which arrive strictly later than their boundaries.
E.g., to illustrate the existence of composites, draw a triangle with A -> B -> C (phase 0 poses the problem) and A -> C (phase 1 delivers the solution).
MSP101 tomorrow 1300 UTC+1
Plans are laid: https://msp.cis.strath.ac.uk/msp101.html
There will be binomial coefficients, bit twiddling, and double categories for beginners like me. All happening live in LT1310 and on zoom if you know where to find us.
Binomial coefficients (m choose n) can be seen as the types of bit vectors with length m, exactly n of which are 1. You can see them as string diagrams from bottom to top, where 1 denotes a wire and 0 connects up but not down. I use them to keep a vice-like grip on variable scope.
Your satnav never says (out loud) "If you're going to ignore me, I don't see the point of persisting with this relationship.".
Do we have a standard written convention for quoting stilted, stitched-together utterances composed by machines from snippets recorded by humans?
"We are/sorry/to announce that/the/six/thirty-seven/CrossCountry/service to/Penzance/is currently running/eleventy/twelve/minutes late./We are laughing our/socks/off."
The price one must learn to pay for proof irrelevance is, funnily enough, not caring what the proof is.
The trick, when you can work it, is to replace inspecting the proof by inspecting the proposition it allegedly justifies. If that proposition is sufficiently plausible, perhaps you can make progress without looking at the proof. Coercion between structurally equal types works just fine on that basis, because "plausibility" is types having the same type constructor.
When is a termination proof plausible enough to allow computation to proceed?
I'm now wondering whether it's worth trying to be clever with some codeBruijn piggery-jokery. Once you cease to be indiscriminately anxious, you might be correspondingly discriminate in your search for reassurance.
By way of further displacement, I rewrote my anxiety-based Boolean prover in Haskell, with a fancy representation for anxiety. https://github.com/pigworker/Samizdat/blob/main/Wang.hs
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.