diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 2fe0b19e5f..6f7824608c 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -33,6 +33,7 @@ open import category-theory.copresheaf-categories public open import category-theory.coproducts-in-precategories public open import category-theory.cores-categories public open import category-theory.cores-precategories public +open import category-theory.coslice-precategories public open import category-theory.dependent-products-of-categories public open import category-theory.dependent-products-of-large-categories public open import category-theory.dependent-products-of-large-precategories public diff --git a/src/category-theory/coslice-precategories.lagda.md b/src/category-theory/coslice-precategories.lagda.md new file mode 100644 index 0000000000..4c41e94cd6 --- /dev/null +++ b/src/category-theory/coslice-precategories.lagda.md @@ -0,0 +1,35 @@ +# Coslice precategories + +```agda +module category-theory.coslice-precategories where +``` + +
Imports + +```agda +open import category-theory.opposite-precategories +open import category-theory.precategories +open import category-theory.slice-precategories + +open import foundation.universe-levels +``` + +
+ +## Idea + +The {{#concept "coslice precategory" Agda=Coslice-Precategory}} of a +[precategory](category-theory.precategories.md) `C` under an object `X` of `C` +is the category of objects of `C` equipped with a morphism from `X`. + +## Definitions + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) (X : obj-Precategory C) + where + + Coslice-Precategory : Precategory (l1 ⊔ l2) l2 + Coslice-Precategory = + Slice-Precategory (opposite-Precategory C) X +``` diff --git a/src/elementary-number-theory/inequality-natural-numbers.lagda.md b/src/elementary-number-theory/inequality-natural-numbers.lagda.md index c2d8117480..90bb0aa048 100644 --- a/src/elementary-number-theory/inequality-natural-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-natural-numbers.lagda.md @@ -7,6 +7,8 @@ module elementary-number-theory.inequality-natural-numbers where
Imports ```agda +open import category-theory.precategories + open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers @@ -147,6 +149,13 @@ pr1 ℕ-Poset = ℕ-Preorder pr2 ℕ-Poset = antisymmetric-leq-ℕ ``` +### The precategory of natural numbers ordered by inequality + +```agda +ℕ-Precategory : Precategory lzero lzero +ℕ-Precategory = precategory-Preorder ℕ-Preorder +``` + ### For any two natural numbers we can decide which one is less than the other ```agda diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 1ce9b78699..de476c0b14 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -82,6 +82,7 @@ open import order-theory.order-preserving-maps-large-posets public open import order-theory.order-preserving-maps-large-preorders public open import order-theory.order-preserving-maps-posets public open import order-theory.order-preserving-maps-preorders public +open import order-theory.ordinals public open import order-theory.posets public open import order-theory.powers-of-large-locales public open import order-theory.precategory-of-decidable-total-orders public diff --git a/src/order-theory/ordinals.lagda.md b/src/order-theory/ordinals.lagda.md new file mode 100644 index 0000000000..06b3979006 --- /dev/null +++ b/src/order-theory/ordinals.lagda.md @@ -0,0 +1,101 @@ +# Ordinals + +```agda +module order-theory.ordinals where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import order-theory.well-founded-orders +open import order-theory.well-founded-relations +``` + +
+ +## Idea + +An ordinal is a propositional relation that is + +- Transitive: `R x y` and `R y z` imply `R x y`. +- Extensional: `R x y` and `R y x` imply `x ＝ y`. +- Well-founded: a structure on which it is well-defined to do induction. + +In other words, it is a +[well-founded order](order-theory.well-founded-orders.md) that is `Prop`-valued +and antisymmetric. + +## Definitions + +### The predicate of being an ordinal + +```agda +module _ + {l1 l2 : Level} {X : UU l1} (R : Relation-Prop l2 X) + where + + is-ordinal : UU (l1 ⊔ l2) + is-ordinal = + is-well-founded-order-Relation (type-Relation-Prop R) × + is-antisymmetric (type-Relation-Prop R) +``` + +### Ordinals + +```agda +Ordinal : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +Ordinal l2 X = Σ (Relation-Prop l2 X) is-ordinal + +module _ + {l1 l2 : Level} {X : UU l1} (S : Ordinal l2 X) + where + + lt-prop-Ordinal : Relation-Prop l2 X + lt-prop-Ordinal = pr1 S + + lt-Ordinal : Relation l2 X + lt-Ordinal = type-Relation-Prop lt-prop-Ordinal + + is-ordinal-Ordinal : + is-ordinal lt-prop-Ordinal + is-ordinal-Ordinal = pr2 S + + is-well-founded-order-Ordinal : + is-well-founded-order-Relation lt-Ordinal + is-well-founded-order-Ordinal = pr1 is-ordinal-Ordinal + + is-antisymmetric-Ordinal : + is-antisymmetric lt-Ordinal + is-antisymmetric-Ordinal = pr2 is-ordinal-Ordinal + + is-transitive-Ordinal : is-transitive lt-Ordinal + is-transitive-Ordinal = + pr1 is-well-founded-order-Ordinal + + is-well-founded-relation-Ordinal : + is-well-founded-Relation lt-Ordinal + is-well-founded-relation-Ordinal = + pr2 is-well-founded-order-Ordinal + + well-founded-relation-Ordinal : Well-Founded-Relation l2 X + pr1 well-founded-relation-Ordinal = + lt-Ordinal + pr2 well-founded-relation-Ordinal = + is-well-founded-relation-Ordinal + + is-asymmetric-Ordinal : + is-asymmetric lt-Ordinal + is-asymmetric-Ordinal = + is-asymmetric-Well-Founded-Relation well-founded-relation-Ordinal + + is-irreflexive-Ordinal : + is-irreflexive lt-Ordinal + is-irreflexive-Ordinal = + is-irreflexive-Well-Founded-Relation + ( well-founded-relation-Ordinal) +``` diff --git a/src/set-theory/cumulative-hierarchy.lagda.md b/src/set-theory/cumulative-hierarchy.lagda.md index 21ef6a5ae8..96fe1b0e32 100644 --- a/src/set-theory/cumulative-hierarchy.lagda.md +++ b/src/set-theory/cumulative-hierarchy.lagda.md @@ -38,8 +38,8 @@ open import foundation.universe-levels ## Idea The cumulative hierarchy is a model of set theory. Instead of introducing it as -a HIT, as in the HoTT Book Section 10.4, we introduce its induction principle, -following Reference 2 below. +a HIT, as in Section 10.4 of {{#cite UF13}}, we introduce its induction +principle, following {{#cite dJKFX23}}. ## Definitions