weak function extensionality without univalence axiom

Stream: general

[deepest recursion]

hi, it looks like it's possible to define weak function extensionality without assuming univalence.
Lean4WebDownload.lean
Can somebody please double check this? The difinition name is wfunext.

(I coldnt paste the link to lean web editor because its too big for zulip)

[Kenny Lau]

you don't need to link to the editor if you just include the code here using #backticks , which automatically generates a link on the top right corner of the code block

[Floris van Doorn]

It is well-known that the existence of quotients gives function extensionality, see e.g. Lemma 6.3.2 of the Homotopy Type theory book.

[deepest recursion]

Does it give univalence too?

[deepest recursion]

The point was that it DOESN'T use univalence, not that its a NOVELL result

[Floris van Doorn]

It's a nice result, and if you discovered it independently: good job.

[James E Hanson]

deepest recursion said:

Does it give univalence too?

It definitely can't because existence of quotients is consistent with axiom K (i.e., uniqueness of identity proofs).

[deepest recursion]

(deleted)

[deepest recursion]

James E Hanson said:

deepest recursion said:

Does it give univalence too?

It definitely can't because existence of quotients is consistent with axiom K (i.e., uniqueness of identity proofs).

it was a play, alright?

[Jean Abou Samra]

deepest recursion said:

it was a play, alright?

I don't understand what "play" you are referring to.

[Jean Abou Samra]

Note that univalence is outright inconsistent in Lean (because it bakes proof irrelevance and hence uniqueness of identity proofs into the core type theory), so no consistent axioms (like quotients) can give you univalence.