Connectives

[fangyi-zhou]

• 初译
• 初校

[OlingCat]

新格式请参考 https://github.com/Agda-zh/PLFA-zh/blob/dev/src/plfa/Induction.lagda
旧有的格式 merge 起来太不友好了，我会慢慢迁移过去。

[chirsz-ever]

本章中所有“up to isomorphism”建议译为“在同构意义下”而不是“忽略同构”；同理，“up to renaming”建议译为“只是换了个名字”。

[chirsz-ever]

第1031行

PLFA-zh/src/plfa/Connectives.lagda

Line 1031 in bb87c79

类型 `B` 有 `n` 个不同的成员，那么类型 `A × B` 有 `nᵐ` 个不同的成员。

应改为

...那么类型 `A → B` 有 `nᵐ` 个不同的成员。

本来想提PR的，但不知为何compare时总会出现大段不相干修改。

[OlingCat]

第1031行

PLFA-zh/src/plfa/Connectives.lagda

Line 1031 in bb87c79

类型 `B` 有 `n` 个不同的成员，那么类型 `A × B` 有 `nᵐ` 个不同的成员。

应改为

...那么类型 `A → B` 有 `nᵐ` 个不同的成员。

本来想提PR的，但不知为何compare时总会出现大段不相干修改。

OK，已修复