What is the difference between the two inductive types
eq in the standard library?
Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A where "x = y :> A" := (@eq A x y) : type_scope.
identity lands in
Type despite this comment:
(** Beware: this inductive actually falls into [Prop], as the sole constructor has no arguments and [-indices-matter] is not activated in the standard library. *)
it used to be in Set but was changed by https://github.com/coq/coq/commit/10fa54f60acdfc8de6b59659f9fa8bc1ed3c18e6
It seems to be in
Check identity. (* identity : forall A : Type, A -> A -> Prop *)
Could we then just deprecate and drop it?
The only useful thing I see is
:tacn:`replace` and :tacn:`inversion` support registration of a :g:`core.identity`\-like equality in :g:`Type`, such as HoTT's :g:`path` (`#12847 <https://github.com/coq/coq/pull/12847>`_, partially fixes `#12846 <https://github.com/coq/coq/issues/12846>`_, by Hugo Herbelin).
does that suggest that
Register foo as core.identity.type (unlike
core.eq.type) would offer support for an equality in
Type rather than
Prop, which is useful in HoTT scenarios?
core.identity.type in the HoTT library for inversion and such.
But we don't use the stdlib one and register our own
Only diff with stdlib is indices-matter
Last updated: Jan 27 2023 at 00:03 UTC