# Weird use of equality in Coq

I have a situation that is kind of like this:

Parameter I : Type.
Parameter V : I -> Type.

Definition convert {k i} (A : V k) (eq : k = i) : V i.
destruct eq.
exact A.
Defined.

Theorem convert_eq : forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
intros i u eq.
unfold convert.
(* Now what? *)

Usually, when working with convert, you can call destruct on the equality being used. However, in this case, trying to use destruct eq gives an error:

Abstracting over the terms "i" and "eq" leads to a term
fun (i0 : I) (eq0 : i0 = i0) => match eq0 in (_ = a) return (V a) with
| eq_refl => u
end = u
which is ill-typed.
Reason is: In pattern-matching on term "eq0" the branch for constructor "eq_refl" has type "V i" which should be
"V i0".

I'll be honest that I've never really been good with these weird uses of equality in definitions, so maybe my whole approach is just wrong. But I feel like convert_eq should be provable somehow. Is there any way to do it?

This kind of thing is possible if equality on I is decidable.

From Coq Require Import Eqdep_dec.

Parameter I : Type.
Parameter V : I -> Type.

Definition convert {k i} (A : V k) (eq : k = i) : V i.
Proof.
destruct eq.
exact A.
Defined.

Axiom eq_dec_I : forall i j : I, i = j \/ i <> j.

Theorem convert_eq : forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
intros i u eq.
replace eq with (eq_refl i).
- now simpl.
- apply eq_proofs_unicity, eq_dec_I.
Qed.

(* alternate proof *)

Theorem convert_eq_2 : forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
intros i u.
apply K_dec.
- apply eq_dec_I.
- now simpl.
Qed.

If you can prove that equality on I is decidable, then great! Replace the axiom above with a theorem, prove the theorem, and you're all set.

If you can't prove that equality on I is decidable, then you could of course assume the law of the excluded middle. Or you could assume/prove a weaker property such as proof irrelevance, or Streicher's Axiom K. See Coq and Axioms.

• Decidability is a sufficient condition, but not necessary. As long as I is a set in the sense of homotopy type theory, i.e., it satisfies the K axiom, you can prove the statement. Commented May 1, 2023 at 9:54
• Thanks! Edited for correctness.
– djao
Commented May 1, 2023 at 12:00
• Well, since you say "in general", that still runs the danger that someone will think it's necessary. How about "This kind of thing is possible if equality on I is decidable"? Commented May 1, 2023 at 12:14
• Sure, that's a good idea.
– djao
Commented May 1, 2023 at 12:41

Welcome to homotopy type theory. What if eq : i = i in convert_eq is not refl? Then conversion along eq could do something nontrivial to u.

The lemma convert_eq can be proved under the additional assumption that I is a set (in the sense of homotopy type theory). (In fact, it is equivalent ot the assumption that I is a set, but I am too lazy to formalize that.)

Parameter I : Type.
Parameter V : I -> Type.

Definition convert {k i} (A : V k) (eq : k = i) : V i.
destruct eq.
exact A.
Defined.

(** A set is a type whose identity types are propositions (have at most one element). *)
Definition is_set (B : Type) := forall (x y : B) (p q : x = y), p = q.

(** Note: a type with decidable equality is a set, see HoTT book 7.2.5. *)

(** Now can prove the lemma under the additional assumption. *)
Theorem convert_eq : is_set I -> forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
intros setI i u eq.
rewrite (setI i i eq eq_refl).
reflexivity.
Qed.

An example of a type which is a set but its equality cannot be shown to be decidable is nat -> nat.

• Possibly a stupid question, but is a Set in Coq a set? (Could we just change the first line to Parameter I : Set.)
– djao
Commented May 1, 2023 at 12:07
• Nope, Set is Type₀, i.e., the lowest level of type hierachy (if we ignore Prop). It's called Set for historical reasons. Martin-Löf originally conceived type theory as a formal system for Bishop's mathematics (which is based on sets), and also people used to think of types as "some sort of sets" before HoTT. Commented May 1, 2023 at 12:12