Narration flow of sections 3.1 and 3.2

[jauzatopauza]

Currently, the narration flow of sections 3.1 and 3.2 is nonsensical. The problem is apparent in the first sentence of section 3.2.

Now, let’s remove all terms from typing rules above, replace × with ∧, + with ∨, and squint our eyes a little.

The “typing rules above” do not involve pairs or copairs, only function types and base types. The section goes like this: 3.1 introduces typing rules for function types and base types, after which 3.2 shows natural deduction including conjunctions and disjunctions, and only then rules for pairs and copairs are presented. This is pretty chaotic, and the aforementioned sentence exposes this chaos even more clearly.

As we also want to add top and bottom types to this section (issue #18), I guess we should take one of the following paths:

1. Introduce all the constructs with their typing rules and reduction rules in 3.1, then reveal the isomorphism with natural deduction in 3.2. This probably requires less text, but might be overwhelming for the reader.
2. Keep 3.1 as it is, show natural deduction with implications only in 3.2 first, and then gradually introduce pairs, copairs, top and bottom together with their propositional counterparts. Here, I am not sure if ”Curry-Howard Isomorphism” still is an appropriate name for such a section, because there would be much more going on inside. However, the introduction of pairs and copairs can be framed as motivated by the isomorphism.

[ppolesiuk]

I'm aware of this problem. It comes from the fact that Mikołaj typeset definitions, probably having approach 1 in mind, but I decided that it would be overwhelming for the reader, and moved some some definitions to the next section without changing the prose. I agree that we should follow path 2.

Here, I am not sure if ”Curry-Howard Isomorphism” still is an appropriate name for such a section, because there would be much more going on inside. However, the introduction of pairs and copairs can be framed as motivated by the isomorphism.

Sure, we can change the name of the section. You can propose a new name, or just change to for instance "Other Constructs and Curry-Howard Isomorphism".