Code

Basic Order Theory#1154

Code

Open

LuuBluum wants to merge 36 commits intoagda:masteragda/cubical:masterfrom LuuBluum:OrderTheoryLuuBluum/cubical:OrderTheoryCopy head branch name to clipboard

+3,900-890

Commits

Commits on Sep 7, 2024

• Add inverses to monoids/comm monoids

  LuuBluum

  committed
  8aac569

  Copy full SHA for 8aac569

• Add meets and joins to order properties

  LuuBluum

  committed
  3e72b31

  Copy full SHA for 3e72b31

• Rewrite isConnected and rename isStronglyConnected

  LuuBluum

  committed
  c276de5

  Copy full SHA for c276de5

• Decidable total and linear orders imply discrete

  LuuBluum

  committed
  fe42e88

  Copy full SHA for fe42e88

• Remove discrete requirement

  LuuBluum

  committed
  3776d2d

  Copy full SHA for 3776d2d

• Move decidable->discrete from toset to poset

  LuuBluum

  committed
  12449c3

  Copy full SHA for 12449c3

• Define binary meets/joins and prove properties

  LuuBluum

  committed
  a3bc329

  Copy full SHA for a3bc329

• The negation of a linear order is a poset

  LuuBluum

  committed
  6b55d8b

  Copy full SHA for 6b55d8b

• Define bounds on a poset

  LuuBluum

  committed
  20be82d

  Copy full SHA for 20be82d

• Mild refactoring

  Show description for ec05705
  LuuBluum

  committed
  ec05705

  Copy full SHA for ec05705

• Remove unnecessary constructors

  LuuBluum

  committed
  fb5049a

  Copy full SHA for fb5049a

• Define tight relations

  LuuBluum

  committed
  5efe05b

  Copy full SHA for 5efe05b

• Reintroduce constructors

  LuuBluum

  committed
  e92681d

  Copy full SHA for e92681d

• Lattice basics

  LuuBluum

  committed
  73a8985

  Copy full SHA for 73a8985

• Distributive lattices

  LuuBluum

  committed
  c8d1ec6

  Copy full SHA for c8d1ec6

• Replace compEquiv usages

  LuuBluum

  committed
  0b06b65

  Copy full SHA for 0b06b65

• Total orders are distributive pseudolattices

  LuuBluum

  committed
  1e85ac9

  Copy full SHA for 1e85ac9

• Add pseudolattice assumption to make more useful

  LuuBluum

  committed
  b06ac86

  Copy full SHA for b06ac86

• Mappings on posets

  LuuBluum

  committed
  d0e8c48

  Copy full SHA for d0e8c48

• Downsets and upsets are preserved

  LuuBluum

  committed
  97c6dec

  Copy full SHA for 97c6dec

• Defined complete lattices

  LuuBluum

  committed
  9d79f2a

  Copy full SHA for 9d79f2a

• Duals and closures

  LuuBluum

  committed
  0b2d8e0

  Copy full SHA for 0b2d8e0

• Embeddings form a complete lattice

  LuuBluum

  committed
  d9f8038

  Copy full SHA for d9f8038

• Dual closures

  LuuBluum

  committed
  b3d0565

  Copy full SHA for b3d0565

• Bicomplete subsets

  LuuBluum

  committed
  321686a

  Copy full SHA for 321686a

• Poset equivalences

  LuuBluum

  committed
  b11149b

  Copy full SHA for b11149b

• Galois connections

  LuuBluum

  committed
  4b2cafb

  Copy full SHA for 4b2cafb

• Fix typo

  LuuBluum

  committed
  96d8ccc

  Copy full SHA for 96d8ccc

• Fix whitespace

  LuuBluum

  committed
  f60761c

  Copy full SHA for f60761c

• Fix build failures

  LuuBluum

  committed
  4d669c1

  Copy full SHA for 4d669c1

Commits on Sep 8, 2024

• Move PosetDownset to where principalDownsets are

  LuuBluum

  committed
  cab1808

  Copy full SHA for cab1808

• Fix build failures

  LuuBluum

  committed
  2b9762c

  Copy full SHA for 2b9762c

• Split mappings and subsets

  LuuBluum

  committed
  f72ba2d

  Copy full SHA for f72ba2d

• Fix whitespace

  LuuBluum

  committed
  6fa2fa6

  Copy full SHA for 6fa2fa6

Commits on Sep 9, 2024

• Proofs regarding residuals and involutions

  LuuBluum

  committed
  ab1e96c

  Copy full SHA for ab1e96c

• Cleaner proof

  LuuBluum

  committed
  2a34d83

  Copy full SHA for 2a34d83