id : ?A → ?A
refl : (?A → ?A → Prop) → Prop
symm : (?A → ?A → Prop) → Prop