Olivier Laurent (Nov 25 2021 at 12:46): Olivier Laurent (Nov 25 2021 at 12:46):What is the difference between the two inductive types identity and eq in the standard library?
Paolo Giarrusso (Nov 25 2021 at 12:49):Good question:
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.
Oh, 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
Olivier Laurent (Nov 25 2021 at 12:54):It seems to be in Prop:
Check identity.
(*
identity
: forall A : Type, A -> A -> Prop
*)
Could we then just deprecate and drop it?
Paolo Giarrusso (Nov 25 2021 at 12:57):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?
Ali Caglayan (Nov 25 2021 at 13:01):We use core.identity.type in the HoTT library for inversion and such.
Paolo Giarrusso (Nov 25 2021 at 13:01):(deleted)
Ali Caglayan (Nov 25 2021 at 13:01):But we don't use the stdlib one and register our own paths type.
Ali Caglayan (Nov 25 2021 at 13:02):Only diff with stdlib is indices-matter
Olivier Laurent (Nov 28 2021 at 09:50):Last updated: Oct 13 2024 at 01:02 UTC