[feature] equivalence

[xieyuheng]

Problem:

We need a built-in type for equivalence.

Solution 1:

Implement "the little typer"-like Equal:

• Equal
• Replace
• Refl
• Same

[ice1000]

I highly recommend a modern identity type (beyond jmeq or mltt id). Quotients and funExt are essential.

[xieyuheng]

Solution 2:

Implement a modern identity type.

(Maybe @ice1000 can suggest something (papers, books, talks, lectures) where we can learn from.)

[ice1000]

I suggest observational equality by McBride or cubical extension type (either cartesian or de morgan)

[xieyuheng]

Solution 1 implemented: https://github.com/cicada-lang/cicada/commit/86e60a30f2e1eafe8876e0cabbd0d71279fc9515

We will explore modern identity type in another issue.

[xieyuheng]

• https://github.com/cicada-lang/cicada/discussions/110