Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor refl : (A : Set) -> (z : A) -> Eq A z z.

I could swear I remember reading somewhere that the equality type was essential in some sense: all other datatypes could be built using it. This would be very useful for dealing with simple dependent type languages, where we don't want to have arbitrary datatypes in our metatheory.

Can someone who knows the field confirm/deny this, or possibly provide a reference?

  • 1
    $\begingroup$ Nope, no idea what you're hinting at. It's an important dependent type, but it is certainly not the case that you can "build all other types" from it. $\endgroup$ – Andrej Bauer Jan 30 '16 at 13:01
  • 1
    $\begingroup$ What you remember is probably the distinction between two presentations of inductive families: the one where indices are constrained in the return type of constructors vs. the one where constructors take an equality proof. $\endgroup$ – gallais Feb 1 '16 at 11:08
  • $\begingroup$ This might actually work for non-recursive data types, when used together with pi and sigma types. $\endgroup$ – Some Axiom Apr 15 '19 at 17:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.