diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index 9f226fa7cc..e2bc34c8a3 100644 --- a/MIXFIX-OPERATORS.md +++ b/MIXFIX-OPERATORS.md @@ -170,7 +170,7 @@ Below, we outline a list of general rules when assigning associativities. | 40 | Multiplicative arithmetic operators | | 36 | Subtractive arithmetic operators | | 35 | Additive arithmetic operators | -| 30 | Relational arithmetic operators, `_≤-ℕ_` and `_<-ℕ_` | +| 30 | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_` | | 25 | Parametric unary operators. This class is currently empty | | 20 | Parametric exponentiative operators. This class is currently empty | | 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, identification concatenation and whiskering operators like `_∙_`, `_∙h_`, `_·l_`, and `_·r_` | diff --git a/src/category-theory/faithful-functors-precategories.lagda.md b/src/category-theory/faithful-functors-precategories.lagda.md index 3552650630..0816a06279 100644 --- a/src/category-theory/faithful-functors-precategories.lagda.md +++ b/src/category-theory/faithful-functors-precategories.lagda.md @@ -28,8 +28,8 @@ A [functor](category-theory.functors-precategories.md) between its an [embedding](foundation-core.embeddings.md) on hom-sets. Note that embeddings on [sets](foundation-core.sets.md) happen to coincide with -[injections](foundation.injective-maps.md), but we define it in terms of the -stronger notion, as this is the notion that generalizes. +[injections](foundation.injective-maps.md). However, we define faithful functors +in terms of embeddings because this is the notion that generalizes. ## Definition @@ -109,7 +109,7 @@ module _ is-prop-is-injective-hom-map-Precategory ``` -### The predicate of being faithful on functors between precategories +### The predicate of being injective on hom-sets on functors between precategories ```agda module _ diff --git a/src/category-theory/presheaf-categories.lagda.md b/src/category-theory/presheaf-categories.lagda.md index df9a811105..f5e7ddd193 100644 --- a/src/category-theory/presheaf-categories.lagda.md +++ b/src/category-theory/presheaf-categories.lagda.md @@ -40,7 +40,7 @@ functor category C → Set. ``` -## Definition +## Definitions ### The copresheaf category of a precategory diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 065549cb7c..aea0990e94 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -29,6 +29,7 @@ open import elementary-number-theory.congruence-integers public open import elementary-number-theory.congruence-natural-numbers public open import elementary-number-theory.decidable-dependent-function-types public open import elementary-number-theory.decidable-total-order-natural-numbers public +open import elementary-number-theory.decidable-total-order-standard-finite-types public open import elementary-number-theory.decidable-types public open import elementary-number-theory.difference-integers public open import elementary-number-theory.dirichlet-convolution public diff --git a/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md b/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md index cf78618350..218c186e1f 100644 --- a/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md +++ b/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md @@ -1,4 +1,4 @@ -# Natural numbers are a total decidable poset +# The decidable total order of natural numbers ```agda module elementary-number-theory.decidable-total-order-natural-numbers where @@ -14,21 +14,30 @@ open import foundation.propositional-truncations open import foundation.universe-levels open import order-theory.decidable-total-orders +open import order-theory.total-orders ``` ## Idea -The type of natural numbers equipped with its standard ordering relation forms a -total order. +The type of [natural numbers](elementary-number-theory.natural-numbers.md) +[equipped](foundation.structure.md) with its +[standard ordering relation](elementary-number-theory.inequality-natural-numbers.md) +forms a [decidable total order](order-theory.decidable-total-orders.md). ## Definition ```agda -ℕ-Decidable-Total-Order : - Decidable-Total-Order lzero lzero +is-total-leq-ℕ : is-total-Poset ℕ-Poset +is-total-leq-ℕ n m = unit-trunc-Prop (linear-leq-ℕ n m) + +ℕ-Total-Order : Total-Order lzero lzero +pr1 ℕ-Total-Order = ℕ-Poset +pr2 ℕ-Total-Order = is-total-leq-ℕ + +ℕ-Decidable-Total-Order : Decidable-Total-Order lzero lzero pr1 ℕ-Decidable-Total-Order = ℕ-Poset -pr1 (pr2 ℕ-Decidable-Total-Order) n m = unit-trunc-Prop (linear-leq-ℕ n m) +pr1 (pr2 ℕ-Decidable-Total-Order) = is-total-leq-ℕ pr2 (pr2 ℕ-Decidable-Total-Order) = is-decidable-leq-ℕ ``` diff --git a/src/elementary-number-theory/decidable-total-order-standard-finite-types.lagda.md b/src/elementary-number-theory/decidable-total-order-standard-finite-types.lagda.md new file mode 100644 index 0000000000..faaf8df86a --- /dev/null +++ b/src/elementary-number-theory/decidable-total-order-standard-finite-types.lagda.md @@ -0,0 +1,47 @@ +# The decidable total order of a standard finite type + +```agda +module elementary-number-theory.decidable-total-order-standard-finite-types where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.inequality-standard-finite-types +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.propositional-truncations +open import foundation.universe-levels + +open import order-theory.decidable-total-orders +open import order-theory.total-orders + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The [standard finite type](univalent-combinatorics.standard-finite-types.md) of +order `k` [equipped](foundation.structure.md) with its +[standard ordering relation](elementary-number-theory.inequality-standard-finite-types.md) +forms a [decidable total order](order-theory.decidable-total-orders.md). + +## Definition + +```agda +is-total-leq-Fin : (k : ℕ) → is-total-Poset (Fin-Poset k) +is-total-leq-Fin k n m = unit-trunc-Prop (linear-leq-Fin k n m) + +Fin-Total-Order : ℕ → Total-Order lzero lzero +pr1 (Fin-Total-Order k) = Fin-Poset k +pr2 (Fin-Total-Order k) = is-total-leq-Fin k + +Fin-Decidable-Total-Order : ℕ → Decidable-Total-Order lzero lzero +pr1 (Fin-Decidable-Total-Order k) = Fin-Poset k +pr1 (pr2 (Fin-Decidable-Total-Order k)) = is-total-leq-Fin k +pr2 (pr2 (Fin-Decidable-Total-Order k)) = is-decidable-leq-Fin k +``` diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md index aa92163af9..edf5188c06 100644 --- a/src/elementary-number-theory/inequality-integers.lagda.md +++ b/src/elementary-number-theory/inequality-integers.lagda.md @@ -37,6 +37,9 @@ leq-ℤ x y = type-Prop (leq-ℤ-Prop x y) is-prop-leq-ℤ : (x y : ℤ) → is-prop (leq-ℤ x y) is-prop-leq-ℤ x y = is-prop-type-Prop (leq-ℤ-Prop x y) + +infix 30 _≤-ℤ_ +_≤-ℤ_ = leq-ℤ ``` ## Properties diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index a06ee851f8..aa52e54c68 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -36,6 +36,9 @@ leq-ℚ x y = type-Prop (leq-ℚ-Prop x y) is-prop-leq-ℚ : (x y : ℚ) → is-prop (leq-ℚ x y) is-prop-leq-ℚ x y = is-prop-type-Prop (leq-ℚ-Prop x y) + +infix 30 _≤-ℚ_ +_≤-ℚ_ = leq-ℚ ``` ### Strict inequality on the rational numbers diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index a5dce189b2..8a095640d1 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md @@ -25,6 +25,7 @@ open import foundation.universe-levels open import order-theory.posets open import order-theory.preorders +open import order-theory.total-orders open import univalent-combinatorics.standard-finite-types ``` @@ -104,9 +105,7 @@ reflects-leq-nat-Fin (succ-ℕ k) {inl x} {inr star} H = star reflects-leq-nat-Fin (succ-ℕ k) {inr star} {inr star} H = star ``` -## Properties - -### The preordering on the standard finite types +### The partial order on the standard finite types ```agda Fin-Preorder : ℕ → Preorder lzero lzero @@ -120,6 +119,8 @@ pr1 (Fin-Poset k) = Fin-Preorder k pr2 (Fin-Poset k) = antisymmetric-leq-Fin k ``` +## Properties + ### Ordering on the standard finite types is decidable ```agda @@ -134,3 +135,12 @@ pr1 (leq-Fin-Decidable-Prop k x y) = leq-Fin k x y pr1 (pr2 (leq-Fin-Decidable-Prop k x y)) = is-prop-leq-Fin k x y pr2 (pr2 (leq-Fin-Decidable-Prop k x y)) = is-decidable-leq-Fin k x y ``` + +### Ordering on the standard finite types is linear + +```agda +linear-leq-Fin : (k : ℕ) (x y : Fin k) → leq-Fin k x y + leq-Fin k y x +linear-leq-Fin (succ-ℕ k) (inl x) (inl y) = linear-leq-Fin k x y +linear-leq-Fin (succ-ℕ k) (inl x) (inr y) = inl star +linear-leq-Fin (succ-ℕ k) (inr x) y = inr star +``` diff --git a/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md b/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md index 3f223b5b5c..80761f26c3 100644 --- a/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md +++ b/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md @@ -18,7 +18,7 @@ open import foundation.universe-levels ## Idea -The ordinal induction principle of the natural numbers is the well-founded +The **ordinal induction principle of the natural numbers** is the well-founded induction principle of ℕ. ## To Do diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md index a877b39fb7..b39c7659d1 100644 --- a/src/order-theory/decidable-total-orders.lagda.md +++ b/src/order-theory/decidable-total-orders.lagda.md @@ -28,8 +28,9 @@ open import order-theory.total-orders ## Idea -A **decidable total order** is a total order of which the inequality relation is -decidable. +A **decidable total order** is a [total order](order-theory.total-orders.md) of +which the inequality [relation](foundation.binary-relations.md) is +[decidable](foundation.decidable-relations.md). ## Definitions diff --git a/src/order-theory/total-orders.lagda.md b/src/order-theory/total-orders.lagda.md index 1c8933f9c7..5c6541a1c9 100644 --- a/src/order-theory/total-orders.lagda.md +++ b/src/order-theory/total-orders.lagda.md @@ -23,9 +23,10 @@ open import order-theory.total-preorders ## Idea -A **total order**, or a \*\*linear order, is a poset `P` such that for every two -elements `x` and `y` in `P` the disjunction `(x ≤ y) ∨ (y ≤ x)` holds. In other -words, total orders are totally ordered in the sense tat any two elements are +A **total order**, or a **linear order**, is a [poset](order-theory.posets.md) +`P` such that for every two elements `x` and `y` in `P` the +[disjunction](foundation.disjunction.md) `(x ≤ y) ∨ (y ≤ x)` holds. In other +words, total orders are totally ordered in the sense that any two elements are comparable. ## Definitions @@ -57,7 +58,7 @@ module _ is-prop-is-total-Poset = is-prop-is-total-Preorder (preorder-Poset X) ``` -### Type of total posets +### The type of total orders ```agda Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) diff --git a/src/set-theory/cardinalities.lagda.md b/src/set-theory/cardinalities.lagda.md index 2ffbf22310..4d34964701 100644 --- a/src/set-theory/cardinalities.lagda.md +++ b/src/set-theory/cardinalities.lagda.md @@ -78,19 +78,15 @@ leq-cardinality-Prop {l1} {l2} = leq-cardinality : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) leq-cardinality X Y = type-Prop (leq-cardinality-Prop X Y) -infix 6 _≤-cardinality_ -_≤-cardinality_ : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) -_≤-cardinality_ = leq-cardinality - is-prop-leq-cardinality : {l1 l2 : Level} {X : cardinal l1} {Y : cardinal l2} → - is-prop (X ≤-cardinality Y) + is-prop (leq-cardinality X Y) is-prop-leq-cardinality {X = X} {Y = Y} = is-prop-type-Prop (leq-cardinality-Prop X Y) compute-leq-cardinality : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - ( cardinality X ≤-cardinality cardinality Y) ≃ + ( leq-cardinality (cardinality X) (cardinality Y)) ≃ ( mere-emb (type-Set X) (type-Set Y)) compute-leq-cardinality {l1} {l2} X Y = equiv-eq-Prop @@ -102,12 +98,14 @@ compute-leq-cardinality {l1} {l2} X Y = unit-leq-cardinality : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - mere-emb (type-Set X) (type-Set Y) → cardinality X ≤-cardinality cardinality Y + mere-emb (type-Set X) (type-Set Y) → + leq-cardinality (cardinality X) (cardinality Y) unit-leq-cardinality X Y = map-inv-equiv (compute-leq-cardinality X Y) inv-unit-leq-cardinality : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - cardinality X ≤-cardinality cardinality Y → mere-emb (type-Set X) (type-Set Y) + leq-cardinality (cardinality X) (cardinality Y) → + mere-emb (type-Set X) (type-Set Y) inv-unit-leq-cardinality X Y = pr1 (compute-leq-cardinality X Y) refl-leq-cardinality : {l : Level} → is-reflexive (leq-cardinality {l}) @@ -121,32 +119,32 @@ transitive-leq-cardinality : (X : cardinal l1) (Y : cardinal l2) (Z : cardinal l3) → - X ≤-cardinality Y → - Y ≤-cardinality Z → - X ≤-cardinality Z + leq-cardinality X Y → + leq-cardinality Y Z → + leq-cardinality X Z transitive-leq-cardinality X Y Z = apply-dependent-universal-property-trunc-Set' (λ u → set-Prop (function-Prop - (u ≤-cardinality Y) - (function-Prop (Y ≤-cardinality Z) + (leq-cardinality u Y) + (function-Prop (leq-cardinality Y Z) (leq-cardinality-Prop u Z)))) (λ a → apply-dependent-universal-property-trunc-Set' (λ v → set-Prop (function-Prop - ((cardinality a) ≤-cardinality v) - (function-Prop (v ≤-cardinality Z) + (leq-cardinality (cardinality a) v) + (function-Prop (leq-cardinality v Z) (leq-cardinality-Prop (cardinality a) Z)))) (λ b → apply-dependent-universal-property-trunc-Set' (λ w → set-Prop (function-Prop - ((cardinality a) ≤-cardinality (cardinality b)) - (function-Prop ((cardinality b) ≤-cardinality w) + (leq-cardinality (cardinality a) (cardinality b)) + (function-Prop (leq-cardinality (cardinality b) w) (leq-cardinality-Prop (cardinality a) w)))) (λ c a