Made the code compatible with the Agda branch issue4786

[nad]

This commit makes the code compatible with what might become a development version of Agda, without breaking compatibility with the current development version.

[nad]

I disabled an example that type-checks very slowly, if at all, using the variant of Agda from the branch issue4786:

cubical/Cubical/Data/DescendingList/Examples.agda

Lines 91 to 92 in 367f3af

	l3=l2++l1 : l3 ≡ l2 ++ᴰᴸ l1
	l3=l2++l1 = refl

The slowdown seems to be caused by the changes on that branch. However, another recent development version of Agda (2.6.3-edd8334) also has trouble normalising the type of this example, unlike Agda 2.6.2. Perhaps it would make sense to figure out what, exactly, has made Agda slower.

[Saizan]

Can you try adding --experimental-lossy-unification to that file? I believe the example is quite fast on a recent agda/master with that flag on.

[nad]

That makes the example type-check quickly. However, Agda still has trouble normalising the goal type.

[Saizan]

Yeah, I don't think it's reasonable to normalize the goal type here, you get quite large transports when you do.

[nad]

It works fine with Agda 2.6.2.

[Saizan]

That's because transports of indexed families are stuck in Agda 2.6.2.

[nad]

OK, that explains the slowdown.