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?