logical equivalence between weakfunext and funext

[emilyriehl]

I spoke just now with Matthias Hutzler who plans to work on this issue, which I'll describe here.

In the contractibility file we define WeakFunExt. We should show that FunExt implies WeakFunExt and conversely.

We might consider cutting all the code

"

For future reference we add a variable we can assume.

#assume weakfunext : WeakFunExt

Whenever a definition (implicitly) uses function extensionality, we write
#!rzk uses (weakfunext).

#def call-weakfunext uses (weakfunext)
  ( A : U )
  ( C : A → U)
  ( f : (a : A) → is-contr (C a) )
  : (is-contr ( (a : A) → C a ))
  := weakfunext A C f

"

because we don't actually use the function call-weakfunext. We shouldn't state assumptions of either funext or weakfunext while demonstrating they are logically equivalent. Instead the goal is to fill in a proof of the following

#def weakfunext-funext
   (funext : FunExt)
   : WeakFunExt
   := ???

and conversely.

[MatthiasHu]

Yes, thank you, I am looking at this!

[MatthiasHu]

I just opened a draft pull request (#74). One direction is done so far. :-)

[emilyriehl]

@TashiWalde and I were discussing the naive form of funext

NaiveFunExt : U
NaiveFunExt := (A : U) -> (B : A -> U) -> (f g : (x : A) -> B x) -> (p : (x : A) -> f x = g x) -> (f = g)

I incorrectly claimed that this was weaker than FunExt but I've discovered I was wrong.

Claim: @MatthiasHu's proof that FunExt -> WeakFunExt in fact shows that NaiveFunExt -> WeakFunExt.

So once he's completed the proof that WeakFunExt -> FunExt we should add NaiveFunExt to the repository (in the equivalences file) and prove the cycle of implications!

[MatthiasHu]

Oh, indeed! 😃

[TashiWalde]

On a tangentially related note, I think that "unique unique choice" is a better name than "weak function extensionality" since it is much more descriptive (and more catchy :) ) . Not sure if its worth changing at this point, just throwing it out there...