I have been using lean for a while and I have noticed that I can't actually prove extensionality for my dependent structures. I was worried at first and then noticed that it was essentially dependent equality that I did not have:
def dependent_equality (X : Type) (A : X → Type) (x : X) (y : X) (p : x = y) : A x = A y := by sorry
X could be
A could be
ℤ/nℤ in the above, in which case I would want an inhabitant of
A n = A m when
n = m. I don't know anything about equal types in Lean, but I was more concerned with certain dependent structures whose corresponding extensionality principals had to be made into axioms.
How does Lean handle dependent equality, or why does it not?
For another more meaningful example, given a structure
S with possibly dependent entries
e₁,...,eₙ, I want to be able to show that
(a₁ : e₁) → (b₁ : e₁) → (a₁ = b₁) → S.mk a₁ = S.mk b₁. With some dependent structures, I have noticed that I can't actually demonstrate extensionality because I get that something isn't "type correct". Meanwhile, it seems that if I was allowed to do multiple rewrites in a row before something was type checked that would solve the problem.
While I am mainly interested in dependent structures up to an equivalence of some kind, I think there are also times where it would be nice to have that property involving