Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The MO question Where do all the projection formulas come from? made me split off a dedicated entry projection formula. Also redirecting reciprocity.
Was there anything usefully different in the earlier question Ubiquity of the push-pull formula and answers?
Oh, I had missed that. Right, that makes what I just posted essentially just a duplicate.
(Thatâ€™s the problem with MO: it will keep reduplicating itself over and over again.)
But it was a chance to advertise dependent linear type theory :)
1 to 4 of 4