2CC Idempotency Elimination

[ibbem]

Create a compiler to eliminate indifferent choices from 2CC

An indifferent choice is a choice like D ⟨ l , l ⟩ where both alternatives are the same. Such choices are often created by compiling CCC→NCC→2CC.
Note about naming: The name redundancy elimination is already taken by the transformation which removed nested choices deciding on the same feature.

[pmbittner]

Maybe, a fitting name would also be idempotence. That is the name of the choice transformation rule D ⟨ l , l ⟩ -> l. I think I would prefer that name for consistency.

Vatras/src/Vatras/Lang/2CC.lagda.md

Lines 147 to 156 in 7aa169b

	{-|
	A choice between two equal alternatives is no choice.
	No matter how we configure the choice, the result stays the same.
	-}
	choice-idempotency : ∀ {D} {e : 2CC Dimension ∞ A}
	---------------------------------
	→ 2CCL Dimension ⊢ D ⟨ e , e ⟩ ≣₁ e
	choice-idempotency {D} {e} c with c D
	... | false = refl
	... | true = refl

[pmbittner]

This looks great! Thank you!