search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
45 stars 12 forks source link

logical equivalence between weakfunext and funext #73

Open emilyriehl opened 1 year ago

emilyriehl commented 1 year ago

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 commented 1 year ago

Yes, thank you, I am looking at this!

MatthiasHu commented 1 year ago

I just opened a draft pull request (https://github.com/rzk-lang/sHoTT/pull/74). One direction is done so far. :-)

emilyriehl commented 1 year ago

@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 commented 1 year ago

Oh, indeed! :smiley:

TashiWalde commented 1 year ago

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...

thchatzidiamantis commented 4 months ago

I've got a proof of the remaining direction, including the discussion about naive-funext (just copying @MatthiasHu's proof as suggested). Things definitely need to be moved (e.g. NaiveFunExt) and renamed.