Write paper that visualizes and explains contraction

[bvssvni]

In the paper "Path Sets", the following example was used:

id[false_1] <=> {false_1, id}

This is somewhat counter-intuitive, since id returns true when the input is true.
Since false_1 returns false for all inputs, it seems natural that id[false_1] => false_1.
How can it be that id[false_1] => id is also a solution?

The key to understand this is that the input is contracted.
When one contracts the input, one is also making a choice.
Here, the choice is to map all inputs to false.

In the normal path, the contracted input is associated with the partial function (false) -> false.
This means that the normal path has a free choice in the partial function (true) -> _.

I think the problem is a feeling of discontinuity between input and output when returning the same value for all inputs.
This intuition is misleading, because the id[false_1] example shows why there really is a continuity.

The only way I can explain this, is that there is an actual contraction of the function id.
The id function is contracted onto (false) -> false.
With other words, the id function "means" (false) -> false in the normal path.