What is the difference between the two inductive types `identity`

and `eq`

in the standard library?

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

It seems to be in `Prop`

:

```
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?

We use `core.identity.type`

in the HoTT library for inversion and such.

(deleted)

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

type.

Only diff with stdlib is indices-matter

Last updated: Jan 27 2023 at 00:03 UTC