search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Proof of Zorn's lemma #281

Closed keltono closed 1 month ago

keltono commented 1 month ago

A proof that the Axiom of Choice implies Zorn's Lemma. Should close or at least partially address issue #178 . Does not provide a proof that Zorn's Lemma (+ LEM) implies the Axiom of choice. This is my first time contributing here (or really doing a substantial formalization project...), so let me know if there are any issues with choice of definitions/style!

ayberkt commented 1 month ago

Thanks @keltono! This is something I've wanted to see in TypeTopology for a long time and I'm happy to see that someone's finally done it.

I'll try to review it as soon as possible, hopefully this weekend.

martinescardo commented 1 month ago

Thanks a lot! I will review this.

martinescardo commented 1 month ago

Looks good! I will do a more thorough review later. For the moment, you should add two more things to your pull request: (1) Your name at the top README.md file, and (2) An import to the index file of the directory your new file is in.

ayberkt commented 1 month ago

@keltono May I also suggest improvements on cosmetic issue that I have noticed? I will do a more proper review later.

  1. Instead of ∥ (x ≪ y + y ≪ x) ∥ can you use ∨ from UF.Logic?
  2. Can you make sure that there are blank lines after \begin{code} and before \end{code}?
keltono commented 1 month ago

Alright, I addressed everything except the point about ∨. I have some thoughts about that: posets don't (necessarily) yield an Omega type, so that information would have to get carried around in proof when it's not really needed, as Zorn's lemma already assumes that ≪ is a poset (and as such x≪y is a proposition) . WIth that said, it seems like ∨ from PropTrunc would be more appropriate, but I seem to be running into an agda parsing bug where agda can't parse x ≪ y ∨ y ≪ x since it's ambiguous if it's UF.PropTrunc.∨ or if it's UF.Logic.∨, even though UF.Logic.∨ is not in scope (since I don't open/import Disjunction), which I haven't been able to resolve by using the fully qualified name. Not sure what's going on there. I have been able to solve this by hiding the PropTrunc ∨ ---which allows me to use the Logic ∨ after importing Disjunction --- but hiding the Logic ∨ doesn't work (since it's not in scope!), so that would force me to use the Logic ∨, which I want to avoid for the reason I mentioned above. There might be some way around this I don't know, I'm not an agda module system expert :).

In any case, I think it's probably fine as is, but you all disagree then it would not be a problem to just switch to the UF.Logic version --- it just feels a little redundant to me.

martinescardo commented 1 month ago

I wonder if you could discuss a complete informal outline of the proof before the formal proof?

Maybe this is not needed if you only explain the main differences with the MO answer.

ayberkt commented 1 month ago

WIth that said, it seems like ∨ from PropTrunc would be more appropriate

Yes sorry, I didn’t mean specifically the one from UF.Logic. Either the one from PropTrunc or UF.Logic is fine. I can try to help you with the parsing problem.

keltono commented 1 month ago

Maybe this is not needed if you only explain the main differences with the MO answer.

After giving it a thorough look through, I think that I was perhaps overselling the differences. The idea is pretty much the same between the two, modulo some particular things about how sets are dealt with in type theory. I changed the comment accordingly.

I was also able to figure out the parsing issue :). I think all of the comments should have been addressed, let me know if there are further points.

martinescardo commented 1 month ago

Thanks again!