We walk through a few proofs of canonicity and normalization, each one with more aspects dissected and re-expressed in category theory, so that readers can compare the difference across proofs. During this process we isolate the different ideas that make up the proofs. Finally we arrive at synthetic Tait computability as proposed by J. Sterling. We also give a synthetic proof for parametricity of system F.

翻译：我们逐步剖析若干典范性与归一化证明，每次以更全面的视角将其解构并重新用范畴论表达，以便读者对比不同证明间的差异。在此过程中，我们分离构成这些证明的不同思想。最终，我们达到J. Sterling提出的合成泰特可计算性，并给出系统F参数性的合成证明。