Cardinality and Order #969

LuuBluum · 2022-12-20T00:15:14Z

Expands upon the existing Poset structure, introducing other forms of orderings to define a preorder over cardinalities. Also includes proofs of Cantor's theorem, for both the general (no surjection into the power set) and the set-specific (an embedding into the power set).

Notably, this includes the definition of an apartness relation, which would be useful for #575 .

felixwellen · 2023-02-02T12:45:56Z

Let me know when it is ready for review (I'm asking because you added commits after marking it ready).

felixwellen · 2023-02-02T12:46:46Z

Interesting stuff!

felixwellen · 2023-02-02T12:52:54Z

I think merging master is a good idea.

LuuBluum · 2023-02-02T16:44:45Z

I think it should be good for review now. Just trying to square away all the names to make sure it's all consistent.

Cubical/Relation/Binary/Order/Properties.agda

maxsnew · 2023-03-10T18:59:04Z

Is this ready? I have a project that uses preorders and might want to base it off of this but don't want to port anything until this is stable

LuuBluum · 2023-03-10T19:05:58Z

Is this ready? I have a project that uses preorders and might want to base it off of this but don't want to port anything until this is stable

Yeah, there's nothing really else for me to add here.

felixwellen · 2023-03-10T19:06:54Z

Next week I should finally have enough time to merge this - sorry for the long wait.

LuuBluum · 2023-03-10T19:07:29Z

Heh, no worries. Didn't help that I kept making changes and that this is a rather sizable PR as it is.

felixwellen

Very nice and useful additions to the library - thanks for that!
Sorry for throwing so much bureaucracy at you, but following conventions and describing things makes it all the more useful for everyone else. Feel free to ignore my request to use more qualified imports if those turn out to be work.
The actual content looks all good to me!

Cubical/Data/Cardinality/Base.agda

felixwellen · 2023-03-23T09:07:31Z

Cubical/Data/FinSet/Induction.agda

@@ -20,7 +20,7 @@ open import Cubical.Data.Nat
  renaming (_+_ to _+ℕ_) hiding (elim)
 open import Cubical.Data.Unit
 open import Cubical.Data.Empty as Empty
-open import Cubical.Data.Sum
+open import Cubical.Data.Sum renaming (⊎-IdR-⊥-≃ to ⊎-⊥-≃)


Please use a qualified import, e.g. "..Sum as Sum" unless there is a good reason not to.

felixwellen · 2023-03-23T09:08:40Z

Cubical/Data/SumFin/Properties.agda

@@ -17,7 +17,7 @@ open import Cubical.Data.Nat.Order
 import Cubical.Data.Fin as Fin
 import Cubical.Data.Fin.LehmerCode as LehmerCode
 open import Cubical.Data.SumFin.Base as SumFin
-open import Cubical.Data.Sum
+open import Cubical.Data.Sum renaming (map to map-⊎; ⊎-IdR-⊥-≃ to ⊎-⊥-≃)


Qualified import?

felixwellen · 2023-03-23T09:18:27Z

Cubical/Functions/Surjection.agda

@@ -91,3 +100,29 @@ compSurjection (f , sur-f) (g , sur-g) =
   λ c → PT.rec isPropPropTrunc
                (λ (b , gb≡c) → PT.rec isPropPropTrunc (λ (a , fa≡b) → ∣ a , (cong g fa≡b ∙ gb≡c) ∣₁) (sur-f b))
                (sur-g c)
+
+-- A slightly more specific form of Lawvere's fixed point theorem


I don't understand the "more specific".

felixwellen · 2023-03-23T09:19:06Z

Cubical/Relation/Binary/Base.agda

 open import Cubical.HITs.SetQuotients.Base
-open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation renaming (rec to ∥₁-rec ; map to ∥₁-map)


qualified import?

Cubical/Relation/Binary/Order/StrictPoset/Base.agda

Cubical/Relation/Binary/Order/Preorder/Base.agda

felixwellen · 2023-03-23T10:26:30Z

Cubical/Relation/Binary/Order/Preorder/Base.agda

+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint


Unused imports?

Cubical/Algebra/CommSemiring/Base.agda

timorl · 2023-06-30T17:27:01Z

Hi! This PR seems to be a bit dead and I would like this to eventually get merged, because I would like to have #286 for some personal work. Thus I'm planning to try dissecting it into a couple smaller PRs and submitting these with the issues from the above comments resolved and more comments in the code (I will be trying to understand everything that is going on myself, so writing down what I figure out shouldn't be too much effort).

I should be able to preserve authorship, but I would still like to know whether @LuuBluum is fine with that or perhaps just wants to finish the PR? So please let me know whether this is a problem.

You probably have quite some time, I have no idea when I'll actually manage to prepare even the first PR.

LuuBluum · 2023-06-30T19:30:06Z

Oh, sorry about that; I should be able to get around to fixing the issues with this. Was just a bit busy with other stuff as of late.

felixwellen · 2023-07-03T15:10:12Z

You have to rebase onto current master (or merge master into your branch) to resolve the conflicts, let me know if you need help doing that (don't know what your background is). I recommend rebasing before you resolve any other problem.

Also cleaned up several aspects of things.

More consistent with the idea of a "subset" and also makes reasoning easier by keeping the sigma types out of the type signatures.

Sigma-types where the type family is always a prop embed into the first argument's type

Also required losets to be weakly linear

LuuBluum · 2023-09-15T18:55:26Z

Alright, finally taking a look at this again.

LuuBluum · 2023-09-15T21:43:55Z

Cleaned up the comments.

felixwellen

Thanks!

Cubical/Relation/Binary/Order/Apartness/Base.agda

Cubical/Relation/Binary/Order/Loset/Base.agda

Cubical/Relation/Binary/Order/Preorder/Base.agda

Cubical/Relation/Binary/Order/StrictPoset/Base.agda

Cubical/Relation/Binary/Order/Toset/Base.agda

* Proof that embeddings are monotone over sums Also cleaned up several aspects of things. * Embeddings are monotone over products * Define cardinal exponentiation * Minor formatting clean-up * Removal of some excessive imports * Renamed annihiliation by 0 to be less vague * Renamed Cantor's Theorem results * Cleaned up order property definitions * Replace renaming * Require preordering for order properties * Remove extra level variable that's unused * Removed redundant implicit level term * Replace type families with embeddings as subtypes More consistent with the idea of a "subset" and also makes reasoning easier by keeping the sigma types out of the type signatures. * Cleaned up types for embeddings in order props * Added function in Embedding to simplify constructs Sigma-types where the type family is always a prop embed into the first argument's type * Minor clean-up * Better respecting camel case * Name-cleaning and removing unused imports * Reintroduce erroneously-removed newline * Renamed loset to toset, strict loset to loset Also required losets to be weakly linear * Fixed paths in top-level file * Defined induced relations over embeddings * Better capitalization * Renamed one more detail * Moved order properties into their own folders * Reduced imports for cardinals * Removed unused apartness import * Changed capitalization back for conversions * Proved induced relations preserve order properties * Loosened embedding to mere function for bounds * Fixed whitespace * Fix rebase issues * Resolve PR comments

LuuBluum force-pushed the Order branch from de01444 to 4771b26 Compare January 13, 2023 22:06

LuuBluum force-pushed the Order branch from 4d9aa2f to 7d156f8 Compare January 22, 2023 05:21

LuuBluum marked this pull request as ready for review January 23, 2023 07:13

LuuBluum mentioned this pull request Jan 28, 2023

The type of reals #286

Open

LuuBluum force-pushed the Order branch from afa3605 to 38e7ae8 Compare February 1, 2023 18:50

felixwellen self-requested a review February 2, 2023 12:44

felixwellen self-assigned this Feb 2, 2023

LuuBluum commented Feb 2, 2023

View reviewed changes

Cubical/Relation/Binary/Order/Properties.agda Outdated Show resolved Hide resolved

felixwellen requested changes Mar 23, 2023

View reviewed changes

LuuBluum added 10 commits September 15, 2023 18:36

Proof that embeddings are monotone over sums

dfec609

Also cleaned up several aspects of things.

Embeddings are monotone over products

6c07acd

Define cardinal exponentiation

a1e5663

Minor formatting clean-up

c0bb7b3

Removal of some excessive imports

03d84e4

Renamed annihiliation by 0 to be less vague

de96a8a

Renamed Cantor's Theorem results

4dc25c9

Cleaned up order property definitions

955fad0

Replace renaming

8ff54f1

Require preordering for order properties

2aa48f6

LuuBluum added 20 commits September 15, 2023 18:38

Removed redundant implicit level term

4abc0bc

Replace type families with embeddings as subtypes

a3d030c

More consistent with the idea of a "subset" and also makes reasoning easier by keeping the sigma types out of the type signatures.

Cleaned up types for embeddings in order props

1446d87

Added function in Embedding to simplify constructs

4f9c7d4

Sigma-types where the type family is always a prop embed into the first argument's type

Minor clean-up

e2524e6

Better respecting camel case

c5dcc00

Name-cleaning and removing unused imports

e661107

Reintroduce erroneously-removed newline

3cdc405

Renamed loset to toset, strict loset to loset

1fbdd22

Also required losets to be weakly linear

Fixed paths in top-level file

429e35b

Defined induced relations over embeddings

2ce1cc3

Better capitalization

d93cdf4

Renamed one more detail

90a0c0d

Moved order properties into their own folders

c96b3e2

Reduced imports for cardinals

a1524a7

Removed unused apartness import

5425f20

Changed capitalization back for conversions

30a72f4

Proved induced relations preserve order properties

858e11a

Loosened embedding to mere function for bounds

7073d1c

Fixed whitespace

9560de1

Fix rebase issues

34c85c9

LuuBluum force-pushed the Order branch from 0138c6d to 34c85c9 Compare September 15, 2023 21:04

Resolve PR comments

144d017

LuuBluum requested a review from felixwellen September 15, 2023 21:45

felixwellen approved these changes Sep 16, 2023

View reviewed changes

felixwellen merged commit 85f8a71 into agda:master Sep 16, 2023

LuuBluum deleted the Order branch October 29, 2023 06:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Cardinality and Order #969

Cardinality and Order #969

LuuBluum commented Dec 20, 2022 •

edited

Loading

felixwellen commented Feb 2, 2023

felixwellen commented Feb 2, 2023

felixwellen commented Feb 2, 2023

LuuBluum commented Feb 2, 2023

maxsnew commented Mar 10, 2023

LuuBluum commented Mar 10, 2023

felixwellen commented Mar 10, 2023

LuuBluum commented Mar 10, 2023

felixwellen left a comment

felixwellen Mar 23, 2023

felixwellen Mar 23, 2023

felixwellen Mar 23, 2023

felixwellen Mar 23, 2023

felixwellen Mar 23, 2023

timorl commented Jun 30, 2023

LuuBluum commented Jun 30, 2023

felixwellen commented Jul 3, 2023

LuuBluum commented Sep 15, 2023

LuuBluum commented Sep 15, 2023

felixwellen left a comment

Cardinality and Order #969

Cardinality and Order #969

Conversation

LuuBluum commented Dec 20, 2022 • edited Loading

felixwellen commented Feb 2, 2023

felixwellen commented Feb 2, 2023

felixwellen commented Feb 2, 2023

LuuBluum commented Feb 2, 2023

maxsnew commented Mar 10, 2023

LuuBluum commented Mar 10, 2023

felixwellen commented Mar 10, 2023

LuuBluum commented Mar 10, 2023

felixwellen left a comment

Choose a reason for hiding this comment

felixwellen Mar 23, 2023

Choose a reason for hiding this comment

felixwellen Mar 23, 2023

Choose a reason for hiding this comment

felixwellen Mar 23, 2023

Choose a reason for hiding this comment

felixwellen Mar 23, 2023

Choose a reason for hiding this comment

felixwellen Mar 23, 2023

Choose a reason for hiding this comment

timorl commented Jun 30, 2023

LuuBluum commented Jun 30, 2023

felixwellen commented Jul 3, 2023

LuuBluum commented Sep 15, 2023

LuuBluum commented Sep 15, 2023

felixwellen left a comment

Choose a reason for hiding this comment

LuuBluum commented Dec 20, 2022 •

edited

Loading