Support propositional equality

[HuStmpHrrr]

We should add propositional equality. There are three terms:

1. Eq A a b which is the type;
2. refl A a is the only constructor;
3. J is the elimination principle; check ITT for an exact formulation.

We need the following things:

• Extend the parser front-end
• Add syntactic rules
  • update syntax for propositional equality #205
  • add rules for prop equality #207
• Add cases for the domain model
  • Add semantics for prop eq #254
• Extend evaluation and readback
  • Add semantics for prop eq #254
• Fix the PER model
  • Add semantics for prop eq #254
  • Eq completeness cases and some optimization #256
• Fix the completeness proof
  • Eq completeness cases and some optimization #256
• Fix the Kripke gluing model
  • Working on soundness proof #259
• Fix the soundness proof
  • Working on soundness proof #259
  • Fix realizability and Lemmas #267
  • add a template for soundness proof #270
  • finished semantic well-formedness of equality type #271
• Fix the typechecker

[HuStmpHrrr]

We use ext/prop-eq for this extension, and then eventually merge it to main.

[HuStmpHrrr]

As per

we do not need to change the subtyping rule at all for equality.

c.f. https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#subtyping-rules

also

Axiom x y : Set.

Definition foo : Type := x.

Axiom bar : @eq Set x y.

Fail Definition baz : @eq Type x y := bar.

This subtyping rule might be too conservative. I intend to believe that we should be able to let subtyping to apply for A in Eq A a b but we should leave this for the future.

[HuStmpHrrr]

thinking about it twice, I think we cannot let subtyping to propagate in any inductive data types. consider just equality. If we allowed subtyping so that if A <: B, then Eq A a b <: Eq B a b, then we immediately lose canonicity of equality. because now refl A a can also be a constructor of Eq B a a, while otherwise, refl B a is the only possible constructor. Clearly, refl A a and refl B a cannot be related. we should really be careful about our intuition with the presence of subtyping.

[Ailrun]

How about contravariant subtyping for pi types? It has a similar problem: \lambda B 5 is of \Pi B \BbbN, but not directly of \Pi A \BbbN (for a subtype A of B)

[HuStmpHrrr]

I tend to believe negative types are better off due to eta expansion. The same probably applies to products.

[Ailrun]

So you mean any positive types should not allow subtyping? Hm, that might be the case...

[Ailrun]

Soundness is not just "tedious". It requires quite a significant change in proofs. For one of simpler examples, we need to change glu_univ_elem_typ_monotone and glu_univ_elem_exp_monotone to be mutually proved.