Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
This alternate formula makes much more sense, thanks! Does it suffice to prove what the old formula was claimed to -- i.e. that (𝐴⊠𝐵)^𝐾 → 𝐴 is a Kan fibration for all K?
Free theorems as I understand it were given based on logical relations not natural transformations (I'm aware of some work sort of relating the two). Do you have a reference for free theorems as natural transformations directly?
