Defining different equality types as inductive typ

Question

I am trying to define in Coq different types of equalities. During an university course my professor gave us the rules of four different types, as follows (I provide just the links to the rules):

• Gentzen : https://ibb.co/imQOCF
• Leibniz : https://ibb.co/n0uBzv
• Martin-Lof : https://ibb.co/fALZKv
• Path Induction : https://ibb.co/esZuKv

The difference among these four types relies on the type C.

I am trying to prove the isomorphism among them. Unfortunately I have some troubles in declaring as inductive types the first and the second, because I cannot find a way to specify the type C. I have a definition for the third and the fourth, and I already proved the isomorphism between them.

Thanks in advance.

Answer 1

You cannot quite use inductive types to obtain something that embodies exactly the first two principles without getting the other two. The reason for that is that Coq inductive data types automatically support strong dependent elimination, which means that the result type is allowed to refer to the element being eliminated. This is what you see in the last two sets of rules you gave: the type C is allowed to refer to a proof p that two points a and b are equal. Any reasonable inductively defined equality type will automatically support rules 3 and 4, and thus 1 and 2, which are weaker. For instance, here's how you get 1 and 2 with Coq's standard equality.

Section Gentzen.

Variables (A : Type) (C : A -> A -> Type).

Definition e_id_g {a b : A} (p : a = b) (c : C a a) : C a b :=
  match p with eq_refl => fun c => c end c.

Definition c_id_g (a : A) (c : C a a) : e_id_g (eq_refl a) c = c :=
  eq_refl.

End Gentzen.

Section Leibniz.

Variables (A : Type) (C : A -> A -> Type).

Definition e_id_l {a b : A} (p : a = b) (c : forall x, C x x) : C a b :=
  match p with eq_refl => c a end.

Definition c_id_l (a : A) (c : forall x, C x x) :
                  e_id_l (eq_refl a) c = c a :=
  eq_refl.

End Leibniz.

It is possible to give a different definition that supports just rules 1 and 2, but not 3 and 4, by using a Church encoding of equality:

Definition eq {A} (a b : A) : Prop :=
  forall P : A -> Prop, P a -> P b.

Definition refl {A} (a : A) : eq a a :=
  fun P x => x.

The idea here -- as in similar encodings for data types in the lambda calculus -- is to define a type as the type of its (non-dependent) eliminator, or fold. This definition is sometimes known as Leibniz equality, and indeed provides essentially the same proof rules as you got in 1 and 2, as the following script shows.

Section Gentzen.

Variables (A : Type) (C : A -> A -> Prop).

Definition e_id_g {a b : A} (p : eq a b) (c : C a a) : C a b :=
  p (C a) c.

Definition c_id_g (a : A) (c : C a a) : e_id_g (refl a) c = c :=
  eq_refl.

End Gentzen.

Section Leibniz.

Variables (A : Type) (C : A -> A -> Prop).

Definition e_id_l {a b : A} (p : eq a b) (c : forall x, C x x) : C a b :=
  p (C a) (c a).

Definition c_id_l (a : A) (c : forall x, C x x) :
                  e_id_l (refl a) c = c a :=
  eq_refl.

End Leibniz.

(These principles are actually a bit different: they are restricted to Prop, due to restrictions in Coq's basic theory related to something called impredicativity. But this is an orthogonal issue.)

Without asserting extra axioms, it is impossible to obtain principles 3 and 4 for this new encoding of equality. Proving this would require doing a case analysis on elements of the type forall P, P a -> P b, and arguing that all these elements are of the form refl applied to something. However, this is a type of functions, and there is no way in Coq's basic theory to perform case analysis on those. Note that this argument lays outside of Coq's theory: it is not contradictory to assert as an extra axiom that 3 and 4 are valid for this new type; it is just impossible to prove so without these axioms.