Stream: Coq users

Topic: [stdlib] identity vs eq


view this post on Zulip Olivier Laurent (Nov 25 2021 at 12:46):

What is the difference between the two inductive types identity and eq in the standard library?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:51):

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. *)

view this post on Zulip Gaƫtan Gilbert (Nov 25 2021 at 12:53):

it used to be in Set but was changed by https://github.com/coq/coq/commit/10fa54f60acdfc8de6b59659f9fa8bc1ed3c18e6

view this post on Zulip Olivier Laurent (Nov 25 2021 at 12:54):

It seems to be in Prop:

Check identity.
(*
identity
     : forall A : Type, A -> A -> Prop
*)

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:56):

Could we then just deprecate and drop it?

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:58):

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?

view this post on Zulip Ali Caglayan (Nov 25 2021 at 13:01):

We use core.identity.type in the HoTT library for inversion and such.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:01):

(deleted)

view this post on Zulip Ali Caglayan (Nov 25 2021 at 13:01):

But we don't use the stdlib one and register our own paths type.

view this post on Zulip Ali Caglayan (Nov 25 2021 at 13:02):

Only diff with stdlib is indices-matter

view this post on Zulip Olivier Laurent (Nov 28 2021 at 09:50):

PR coq/coq#15256


Last updated: Jan 27 2023 at 00:03 UTC