# Errata

 JACM Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACMAfter going to press, we have fixed the following mistakes: In the definition of a logos, we mistakenly said that "colimits commute with finite limits" but we meant to say that they commute with pullbacks. We thank Sarah Rovner-Frydman for noticing this mistake. In Remark 5.15, we used the notation for the closed immersion prior to introducing it. The local copy linked here has the corrections implemented.