mathlib3

66d3f897 - feat(logic/unique): functions from a `unique` type is `const` (#14823)

feat(logic/unique): functions from a `unique` type is `const` (#14823) + A function `f` from a `unique` type is equal to the constant function with value `f default`, and the analogous heq version for dependent functions. + Also changes `Π a : α, Sort v` in the file to `α → Sort v`. Inspired by https://github.com/leanprover-community/mathlib/pull/14724#discussion_r900542203