A Dependently Typed Language with Dynamic Equality lemay-2023-aTyDe · 2023