Code

Cardinality and Order#969

Code

Merged

felixwellen merged 33 commits intoagda:masteragda/cubical:masterfrom LuuBluum:OrderLuuBluum/cubical:OrderCopy head branch name to clipboardSep 16, 2023

+2,044-42

Commits

Commits on Sep 15, 2023

• Proof that embeddings are monotone over sums

  Show description for dfec609
  LuuBluum

  committed
  dfec609

  Copy full SHA for dfec609

• Embeddings are monotone over products

  LuuBluum

  committed
  6c07acd

  Copy full SHA for 6c07acd

• Define cardinal exponentiation

  LuuBluum

  committed
  a1e5663

  Copy full SHA for a1e5663

• Minor formatting clean-up

  LuuBluum

  committed
  c0bb7b3

  Copy full SHA for c0bb7b3

• Removal of some excessive imports

  LuuBluum

  committed
  03d84e4

  Copy full SHA for 03d84e4

• Renamed annihiliation by 0 to be less vague

  LuuBluum

  committed
  de96a8a

  Copy full SHA for de96a8a

• Renamed Cantor's Theorem results

  LuuBluum

  committed
  4dc25c9

  Copy full SHA for 4dc25c9

• Cleaned up order property definitions

  LuuBluum

  committed
  955fad0

  Copy full SHA for 955fad0

• Replace renaming

  LuuBluum

  committed
  8ff54f1

  Copy full SHA for 8ff54f1

• Require preordering for order properties

  LuuBluum

  committed
  2aa48f6

  Copy full SHA for 2aa48f6

• Remove extra level variable that's unused

  LuuBluum

  committed
  efebb95

  Copy full SHA for efebb95

• Removed redundant implicit level term

  LuuBluum

  committed
  4abc0bc

  Copy full SHA for 4abc0bc

• Replace type families with embeddings as subtypes

  Show description for a3d030c
  LuuBluum

  committed
  a3d030c

  Copy full SHA for a3d030c

• Cleaned up types for embeddings in order props

  LuuBluum

  committed
  1446d87

  Copy full SHA for 1446d87

• Added function in Embedding to simplify constructs

  Show description for 4f9c7d4
  LuuBluum

  committed
  4f9c7d4

  Copy full SHA for 4f9c7d4

• Minor clean-up

  LuuBluum

  committed
  e2524e6

  Copy full SHA for e2524e6

• Better respecting camel case

  LuuBluum

  committed
  c5dcc00

  Copy full SHA for c5dcc00

• Name-cleaning and removing unused imports

  LuuBluum

  committed
  e661107

  Copy full SHA for e661107

• Reintroduce erroneously-removed newline

  LuuBluum

  committed
  3cdc405

  Copy full SHA for 3cdc405

• Renamed loset to toset, strict loset to loset

  Show description for 1fbdd22
  LuuBluum

  committed
  1fbdd22

  Copy full SHA for 1fbdd22

• Fixed paths in top-level file

  LuuBluum

  committed
  429e35b

  Copy full SHA for 429e35b

• Defined induced relations over embeddings

  LuuBluum

  committed
  2ce1cc3

  Copy full SHA for 2ce1cc3

• Better capitalization

  LuuBluum

  committed
  d93cdf4

  Copy full SHA for d93cdf4

• Renamed one more detail

  LuuBluum

  committed
  90a0c0d

  Copy full SHA for 90a0c0d

• Moved order properties into their own folders

  LuuBluum

  committed
  c96b3e2

  Copy full SHA for c96b3e2

• Reduced imports for cardinals

  LuuBluum

  committed
  a1524a7

  Copy full SHA for a1524a7

• Removed unused apartness import

  LuuBluum

  committed
  5425f20

  Copy full SHA for 5425f20

• Changed capitalization back for conversions

  LuuBluum

  committed
  30a72f4

  Copy full SHA for 30a72f4

• Proved induced relations preserve order properties

  LuuBluum

  committed
  858e11a

  Copy full SHA for 858e11a

• Loosened embedding to mere function for bounds

  LuuBluum

  committed
  7073d1c

  Copy full SHA for 7073d1c

• Fixed whitespace

  LuuBluum

  committed
  9560de1

  Copy full SHA for 9560de1

• Fix rebase issues

  LuuBluum

  committed
  34c85c9

  Copy full SHA for 34c85c9

• Resolve PR comments

  LuuBluum

  committed
  144d017

  Copy full SHA for 144d017