From 240a8a80ed14d88ce5d15937a2a023dd54b400b7 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 2 Apr 2025 14:53:57 -0400 Subject: [PATCH 1/6] bounded total orders and simplices --- .../bounded-total-orders.lagda.md | 119 ++++++++++++++++++ src/simplicial-type-theory/simplices.lagda.md | 107 ++++++++++++++++ 2 files changed, 226 insertions(+) create mode 100644 src/order-theory/bounded-total-orders.lagda.md create mode 100644 src/simplicial-type-theory/simplices.lagda.md diff --git a/src/order-theory/bounded-total-orders.lagda.md b/src/order-theory/bounded-total-orders.lagda.md new file mode 100644 index 0000000000..53a83da1d4 --- /dev/null +++ b/src/order-theory/bounded-total-orders.lagda.md @@ -0,0 +1,119 @@ +# Bounded total orders + +```agda +module order-theory.bounded-total-orders where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.universe-levels + +open import order-theory.bottom-elements-posets +open import order-theory.posets +open import order-theory.top-elements-posets +open import order-theory.total-orders +``` + +
+ +## Idea + +A bounded total order is a [total order](order-theory.total-orders.md) equipped with a top and bottom element. + +## Definitions + +### The predicate of being a bounded total order + +```agda +module _ + {l1 l2 : Level} (L : Total-Order l1 l2) + where + + is-bounded-Total-Order : UU (l1 ⊔ l2) + is-bounded-Total-Order = + has-top-element-Poset (poset-Total-Order L) × + has-bottom-element-Poset (poset-Total-Order L) +``` + +### Bounded total orders + +```agda +Bounded-Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Bounded-Total-Order l1 l2 = + Σ (Total-Order l1 l2) is-bounded-Total-Order + +module _ + {l1 l2 : Level} (L : Bounded-Total-Order l1 l2) + where + + total-order-Bounded-Total-Order : Total-Order l1 l2 + total-order-Bounded-Total-Order = pr1 L + + poset-Bounded-Total-Order : Poset l1 l2 + poset-Bounded-Total-Order = + poset-Total-Order total-order-Bounded-Total-Order + + type-Bounded-Total-Order : UU l1 + type-Bounded-Total-Order = + type-Total-Order total-order-Bounded-Total-Order + + leq-prop-Bounded-Total-Order : + (x y : type-Bounded-Total-Order) → Prop l2 + leq-prop-Bounded-Total-Order = + leq-prop-Poset poset-Bounded-Total-Order + + leq-Bounded-Total-Order : + (x y : type-Bounded-Total-Order) → UU l2 + leq-Bounded-Total-Order = + leq-Poset poset-Bounded-Total-Order + + refl-leq-Bounded-Total-Order : + is-reflexive leq-Bounded-Total-Order + refl-leq-Bounded-Total-Order = + refl-leq-Poset poset-Bounded-Total-Order + + transitive-leq-Bounded-Total-Order : + is-transitive leq-Bounded-Total-Order + transitive-leq-Bounded-Total-Order = + transitive-leq-Poset poset-Bounded-Total-Order + + antisymmetric-leq-Bounded-Total-Order : + is-antisymmetric leq-Bounded-Total-Order + antisymmetric-leq-Bounded-Total-Order = + antisymmetric-leq-Poset poset-Bounded-Total-Order + + has-top-element-Bounded-Total-Order : + has-top-element-Poset poset-Bounded-Total-Order + has-top-element-Bounded-Total-Order = + pr1 (pr2 L) + + top-Bounded-Total-Order : + type-Bounded-Total-Order + top-Bounded-Total-Order = + pr1 has-top-element-Bounded-Total-Order + + is-top-element-top-Bounded-Total-Order : + is-top-element-Poset poset-Bounded-Total-Order top-Bounded-Total-Order + is-top-element-top-Bounded-Total-Order = + pr2 has-top-element-Bounded-Total-Order + + has-bottom-element-Bounded-Total-Order : + has-bottom-element-Poset poset-Bounded-Total-Order + has-bottom-element-Bounded-Total-Order = + pr2 (pr2 L) + + bottom-Bounded-Total-Order : + type-Bounded-Total-Order + bottom-Bounded-Total-Order = + pr1 has-bottom-element-Bounded-Total-Order + + is-bottom-element-bottom-Bounded-Total-Order : + is-bottom-element-Poset poset-Bounded-Total-Order bottom-Bounded-Total-Order + is-bottom-element-bottom-Bounded-Total-Order = + pr2 has-bottom-element-Bounded-Total-Order +``` diff --git a/src/simplicial-type-theory/simplices.lagda.md b/src/simplicial-type-theory/simplices.lagda.md new file mode 100644 index 0000000000..aeb2a572d3 --- /dev/null +++ b/src/simplicial-type-theory/simplices.lagda.md @@ -0,0 +1,107 @@ +# Simplices + +```agda +module simplicial-type-theory.simplices where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.equality-cartesian-product-types +open import foundation.identity-types +open import foundation.raising-universe-levels +open import foundation.subtypes +open import foundation.unit-type +open import foundation.universe-levels + +open import order-theory.bounded-total-orders +``` + +
+ +## Idea + +Goals + +Formalize +- is-segal +- comp-is-segal +- witness-comp-is-segal +- uniqueness-comp-is-segal +- is-local-horn-inclusion +- The equivalence between is-local-horn-inclusion and is-segal +- is-local-horn-inclusion-function-type +- is-segal-function-type +- trivial identities +- associativity of comp-is-segal + +## Definitions + +```agda +module simplex + {l1 : Level} (I : Bounded-Total-Order l1 l1) + where + + Δ : ℕ → UU l1 + last : (n : ℕ) → Δ (n +ℕ 1) → type-Bounded-Total-Order I + + Δ zero-ℕ = raise-unit l1 + Δ (succ-ℕ zero-ℕ) = type-Bounded-Total-Order I + Δ (succ-ℕ (succ-ℕ n)) = + type-subtype + ( λ ((x , j) : Δ (succ-ℕ n) × type-Bounded-Total-Order I) → + leq-prop-Bounded-Total-Order I j (last n x)) + + last zero-ℕ i = i + last (succ-ℕ n) ((x , j) , H) = j + + eq-Δ-succ-ℕ : + {n : ℕ} (u v : Δ (succ-ℕ (succ-ℕ n))) → + pr1 (pr1 u) ＝ pr1 (pr1 v) → last (succ-ℕ n) u ＝ last (succ-ℕ n) v → u ＝ v + eq-Δ-succ-ℕ {n} u v p q = + eq-type-subtype + ( λ ((x , j) : Δ (succ-ℕ n) × type-Bounded-Total-Order I) → + leq-prop-Bounded-Total-Order I j (last n x)) + ( eq-pair p q) + + d00 : Δ 0 → Δ 1 + d00 (map-raise star) = top-Bounded-Total-Order I + + d01 : Δ 0 → Δ 1 + d01 (map-raise star) = bottom-Bounded-Total-Order I + + d10 : Δ 1 → Δ 2 + pr1 (pr1 (d10 i)) = top-Bounded-Total-Order I + pr2 (pr1 (d10 i)) = i + pr2 (d10 i) = is-top-element-top-Bounded-Total-Order I i + + d11 : Δ 1 → Δ 2 + pr1 (pr1 (d11 i)) = i + pr2 (pr1 (d11 i)) = i + pr2 (d11 i) = refl-leq-Bounded-Total-Order I i + + d12 : Δ 1 → Δ 2 + pr1 (pr1 (d12 i)) = i + pr2 (pr1 (d12 i)) = bottom-Bounded-Total-Order I + pr2 (d12 i) = is-bottom-element-bottom-Bounded-Total-Order I i + + identity-d10-d00 : + (i : Δ 0) → d10 (d00 i) ＝ d11 (d00 i) + identity-d10-d00 (map-raise star) = + eq-Δ-succ-ℕ _ _ refl refl + + identity-d10-d01 : + (i : Δ 0) → d10 (d01 i) ＝ d12 (d00 i) + identity-d10-d01 (map-raise star) = + eq-Δ-succ-ℕ _ _ refl refl + + identity-d11-d01 : + (i : Δ 0) → d11 (d01 i) ＝ d12 (d01 i) + identity-d11-d01 (map-raise star) = + eq-Δ-succ-ℕ _ _ refl refl +``` From d0a63e1661f076d2ca66a142e486c9d3ed184913 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 3 Apr 2025 13:22:44 -0400 Subject: [PATCH 2/6] emily's work --- src/simplicial-type-theory/simplices.lagda.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/simplicial-type-theory/simplices.lagda.md b/src/simplicial-type-theory/simplices.lagda.md index aeb2a572d3..85d216da8e 100644 --- a/src/simplicial-type-theory/simplices.lagda.md +++ b/src/simplicial-type-theory/simplices.lagda.md @@ -29,6 +29,7 @@ open import order-theory.bounded-total-orders Goals Formalize + - is-segal - comp-is-segal - witness-comp-is-segal @@ -49,6 +50,7 @@ module simplex Δ : ℕ → UU l1 last : (n : ℕ) → Δ (n +ℕ 1) → type-Bounded-Total-Order I + initial : (n : ℕ) → Δ (n +ℕ 2) → Δ (n +ℕ 1) Δ zero-ℕ = raise-unit l1 Δ (succ-ℕ zero-ℕ) = type-Bounded-Total-Order I @@ -60,6 +62,8 @@ module simplex last zero-ℕ i = i last (succ-ℕ n) ((x , j) , H) = j + initial n ((x , j) , H) = x + eq-Δ-succ-ℕ : {n : ℕ} (u v : Δ (succ-ℕ (succ-ℕ n))) → pr1 (pr1 u) ＝ pr1 (pr1 v) → last (succ-ℕ n) u ＝ last (succ-ℕ n) v → u ＝ v @@ -104,4 +108,18 @@ module simplex (i : Δ 0) → d11 (d01 i) ＝ d12 (d01 i) identity-d11-d01 (map-raise star) = eq-Δ-succ-ℕ _ _ refl refl + + s00 : Δ 1 → Δ 0 + s00 i = map-raise star + + s10 : Δ 2 → Δ 1 + s10 ((x , j) , H) = j + + s11 : Δ 2 → Δ 1 + s11 p = initial _ p + + identity-s00-s10 : + (p : Δ 2) → s00 (s10 p) ＝ s00 (s11 p) + identity-s00-s10 ((_ , _) , _) = refl + ``` From 262a60e1f31a2c54ea7476b58bf0784427879ca5 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 9 Apr 2025 15:28:41 -0400 Subject: [PATCH 3/6] refactor --- .../bounded-total-orders.lagda.md | 5 + src/simplicial-type-theory/simplices.lagda.md | 128 +++++++++++------- 2 files changed, 86 insertions(+), 47 deletions(-) diff --git a/src/order-theory/bounded-total-orders.lagda.md b/src/order-theory/bounded-total-orders.lagda.md index 53a83da1d4..6b0b46252b 100644 --- a/src/order-theory/bounded-total-orders.lagda.md +++ b/src/order-theory/bounded-total-orders.lagda.md @@ -72,6 +72,11 @@ module _ leq-Bounded-Total-Order = leq-Poset poset-Bounded-Total-Order + is-prop-leq-Bounded-Total-Order : + (x y : type-Bounded-Total-Order) → is-prop (leq-Bounded-Total-Order x y) + is-prop-leq-Bounded-Total-Order = + is-prop-leq-Poset poset-Bounded-Total-Order + refl-leq-Bounded-Total-Order : is-reflexive leq-Bounded-Total-Order refl-leq-Bounded-Total-Order = diff --git a/src/simplicial-type-theory/simplices.lagda.md b/src/simplicial-type-theory/simplices.lagda.md index 85d216da8e..e7a291fd37 100644 --- a/src/simplicial-type-theory/simplices.lagda.md +++ b/src/simplicial-type-theory/simplices.lagda.md @@ -10,10 +10,13 @@ module simplicial-type-theory.simplices where open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import foundation.action-on-identifications-functions +open import foundation.binary-relations open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.identity-types +open import foundation.propositions open import foundation.raising-universe-levels open import foundation.subtypes open import foundation.unit-type @@ -48,78 +51,109 @@ module simplex {l1 : Level} (I : Bounded-Total-Order l1 l1) where - Δ : ℕ → UU l1 - last : (n : ℕ) → Δ (n +ℕ 1) → type-Bounded-Total-Order I - initial : (n : ℕ) → Δ (n +ℕ 2) → Δ (n +ℕ 1) - - Δ zero-ℕ = raise-unit l1 - Δ (succ-ℕ zero-ℕ) = type-Bounded-Total-Order I - Δ (succ-ℕ (succ-ℕ n)) = - type-subtype - ( λ ((x , j) : Δ (succ-ℕ n) × type-Bounded-Total-Order I) → - leq-prop-Bounded-Total-Order I j (last n x)) - - last zero-ℕ i = i - last (succ-ℕ n) ((x , j) , H) = j - - initial n ((x , j) , H) = x - - eq-Δ-succ-ℕ : - {n : ℕ} (u v : Δ (succ-ℕ (succ-ℕ n))) → - pr1 (pr1 u) ＝ pr1 (pr1 v) → last (succ-ℕ n) u ＝ last (succ-ℕ n) v → u ＝ v - eq-Δ-succ-ℕ {n} u v p q = - eq-type-subtype - ( λ ((x , j) : Δ (succ-ℕ n) × type-Bounded-Total-Order I) → - leq-prop-Bounded-Total-Order I j (last n x)) - ( eq-pair p q) + mutual + + data + Δ : ℕ → UU l1 + where + + pt-Δ : Δ 0 + + cons-Δ : + {n : ℕ} (x : Δ n) (i : type-Bounded-Total-Order I) → + (H : leq-Bounded-Total-Order I i (final-Δ n x)) → Δ (succ-ℕ n) + + final-Δ : (n : ℕ) → Δ n → type-Bounded-Total-Order I + final-Δ n pt-Δ = top-Bounded-Total-Order I + final-Δ _ (cons-Δ x i H) = i + + ap-cons-Δ : + {n : ℕ} {x y : Δ n} (p : x ＝ y) + {i j : type-Bounded-Total-Order I} (q : i ＝ j) → + (H : leq-Bounded-Total-Order I i (final-Δ n x)) → + (K : leq-Bounded-Total-Order I j (final-Δ n y)) → + cons-Δ x i H ＝ cons-Δ y j K + ap-cons-Δ refl refl H K = + ap (cons-Δ _ _) (eq-is-prop (is-prop-leq-Bounded-Total-Order I _ _)) + + initial-Δ : (n : ℕ) → Δ (n +ℕ 1) → Δ n + initial-Δ n (cons-Δ x i H) = x + + data + Eq-Δ : (n : ℕ) → Δ n → Δ n → UU l1 + where + + refl-Eq-pt-Δ : Eq-Δ 0 pt-Δ pt-Δ + + Eq-cons-Δ : + {n : ℕ} {x y : Δ n} {i j : type-Bounded-Total-Order I} → + (H : leq-Bounded-Total-Order I i (final-Δ n x)) → + (K : leq-Bounded-Total-Order I j (final-Δ n y)) → + Eq-Δ n x y → i ＝ j → Eq-Δ (succ-ℕ n) (cons-Δ x i H) (cons-Δ y j K) + + refl-Eq-Δ : + {n : ℕ} → is-reflexive (Eq-Δ n) + refl-Eq-Δ pt-Δ = refl-Eq-pt-Δ + refl-Eq-Δ (cons-Δ x i H) = + Eq-cons-Δ H H (refl-Eq-Δ x) refl + + Eq-eq-Δ : + (n : ℕ) (x y : Δ n) → x ＝ y → Eq-Δ n x y + Eq-eq-Δ n x y refl = refl-Eq-Δ x + + eq-Eq-Δ : + {n : ℕ} {x y : Δ n} → Eq-Δ n x y → x ＝ y + eq-Eq-Δ refl-Eq-pt-Δ = refl + eq-Eq-Δ (Eq-cons-Δ H K e refl) = + ap-cons-Δ (eq-Eq-Δ e) refl H K + + in-Δ : type-Bounded-Total-Order I → Δ 1 + in-Δ i = cons-Δ pt-Δ i (is-top-element-top-Bounded-Total-Order I _) d00 : Δ 0 → Δ 1 - d00 (map-raise star) = top-Bounded-Total-Order I + d00 pt-Δ = in-Δ (top-Bounded-Total-Order I) d01 : Δ 0 → Δ 1 - d01 (map-raise star) = bottom-Bounded-Total-Order I + d01 pt-Δ = in-Δ (bottom-Bounded-Total-Order I) d10 : Δ 1 → Δ 2 - pr1 (pr1 (d10 i)) = top-Bounded-Total-Order I - pr2 (pr1 (d10 i)) = i - pr2 (d10 i) = is-top-element-top-Bounded-Total-Order I i + d10 (cons-Δ pt-Δ i H) = + cons-Δ (d00 pt-Δ) i H d11 : Δ 1 → Δ 2 - pr1 (pr1 (d11 i)) = i - pr2 (pr1 (d11 i)) = i - pr2 (d11 i) = refl-leq-Bounded-Total-Order I i + d11 x = cons-Δ x (final-Δ 1 x) (refl-leq-Bounded-Total-Order I _) d12 : Δ 1 → Δ 2 - pr1 (pr1 (d12 i)) = i - pr2 (pr1 (d12 i)) = bottom-Bounded-Total-Order I - pr2 (d12 i) = is-bottom-element-bottom-Bounded-Total-Order I i + d12 x = + cons-Δ x + ( bottom-Bounded-Total-Order I) + ( is-bottom-element-bottom-Bounded-Total-Order I _) identity-d10-d00 : (i : Δ 0) → d10 (d00 i) ＝ d11 (d00 i) - identity-d10-d00 (map-raise star) = - eq-Δ-succ-ℕ _ _ refl refl + identity-d10-d00 pt-Δ = + eq-Eq-Δ (Eq-cons-Δ _ _ (refl-Eq-Δ _) refl) identity-d10-d01 : (i : Δ 0) → d10 (d01 i) ＝ d12 (d00 i) - identity-d10-d01 (map-raise star) = - eq-Δ-succ-ℕ _ _ refl refl + identity-d10-d01 pt-Δ = + eq-Eq-Δ (Eq-cons-Δ _ _ (refl-Eq-Δ _) refl) identity-d11-d01 : (i : Δ 0) → d11 (d01 i) ＝ d12 (d01 i) - identity-d11-d01 (map-raise star) = - eq-Δ-succ-ℕ _ _ refl refl + identity-d11-d01 pt-Δ = + eq-Eq-Δ (Eq-cons-Δ _ _ (refl-Eq-Δ _) refl) s00 : Δ 1 → Δ 0 - s00 i = map-raise star + s00 i = pt-Δ s10 : Δ 2 → Δ 1 - s10 ((x , j) , H) = j + s10 (cons-Δ x i H) = in-Δ i s11 : Δ 2 → Δ 1 - s11 p = initial _ p + s11 x = initial-Δ _ x identity-s00-s10 : - (p : Δ 2) → s00 (s10 p) ＝ s00 (s11 p) - identity-s00-s10 ((_ , _) , _) = refl - + (x : Δ 2) → s00 (s10 x) ＝ s00 (s11 x) + identity-s00-s10 (cons-Δ x i H) = refl ``` From 2fbdff82e5109263d26629ea60b9be283cac3453 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 9 Apr 2025 16:46:22 -0400 Subject: [PATCH 4/6] work --- src/simplicial-type-theory/simplices.lagda.md | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/src/simplicial-type-theory/simplices.lagda.md b/src/simplicial-type-theory/simplices.lagda.md index e7a291fd37..20e4377f97 100644 --- a/src/simplicial-type-theory/simplices.lagda.md +++ b/src/simplicial-type-theory/simplices.lagda.md @@ -15,6 +15,8 @@ open import foundation.binary-relations open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types +open import foundation.equivalences +open import foundation.function-types open import foundation.identity-types open import foundation.propositions open import foundation.raising-universe-levels @@ -23,6 +25,8 @@ open import foundation.unit-type open import foundation.universe-levels open import order-theory.bounded-total-orders + +open import synthetic-homotopy-theory.pushouts ``` @@ -156,4 +160,51 @@ module simplex identity-s00-s10 : (x : Δ 2) → s00 (s10 x) ＝ s00 (s11 x) identity-s00-s10 (cons-Δ x i H) = refl + + module _ + {l : Level} (X : UU l) + where + + nerve-Δ : ℕ → UU (l1 ⊔ l) + nerve-Δ n = Δ n → X + + obj-Δ : UU (l1 ⊔ l) + obj-Δ = nerve-Δ 0 + + mor-Δ : UU (l1 ⊔ l) + mor-Δ = nerve-Δ 1 + + dom-Δ : mor-Δ → obj-Δ + dom-Δ f = f ∘ d01 + + cod-Δ : mor-Δ → obj-Δ + cod-Δ f = f ∘ d00 + + id-mor-Δ : obj-Δ → mor-Δ + id-mor-Δ f = f ∘ s00 + + record + midhorn {l : Level} (X : UU l) : UU (l1 ⊔ l) + where + + constructor + tim + + field + fstmor sndmor : mor-Δ X + compat : cod-Δ X fstmor pt-Δ ＝ dom-Δ X sndmor pt-Δ + + representing-midhorn : UU l1 + representing-midhorn = + pushout d00 d01 + + open midhorn public + + resmid-Δ : {l : Level} {X : UU l} → nerve-Δ X 2 → midhorn X + fstmor (resmid-Δ f) = f ∘ d12 + sndmor (resmid-Δ f) = f ∘ d10 + compat (resmid-Δ f) = ap f (inv (identity-d10-d01 pt-Δ)) + + is-segal : {l : Level} (X : UU l) → UU (l1 ⊔ l) + is-segal X = is-equiv (resmid-Δ {X = X}) ``` From 843f58cf1f10df764f44976f4e3b5835aefda803 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Tue, 15 Apr 2025 15:55:04 -0400 Subject: [PATCH 5/6] equivalence of segal conditions --- src/simplicial-type-theory/simplices.lagda.md | 148 +++++++++++++++--- 1 file changed, 123 insertions(+), 25 deletions(-) diff --git a/src/simplicial-type-theory/simplices.lagda.md b/src/simplicial-type-theory/simplices.lagda.md index 20e4377f97..e1dee4d113 100644 --- a/src/simplicial-type-theory/simplices.lagda.md +++ b/src/simplicial-type-theory/simplices.lagda.md @@ -13,19 +13,26 @@ open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.cartesian-product-types +open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.equivalences open import foundation.function-types +open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.raising-universe-levels +open import foundation.retractions +open import foundation.sections open import foundation.subtypes open import foundation.unit-type open import foundation.universe-levels open import order-theory.bounded-total-orders +open import orthogonal-factorization-systems.extensions-maps +open import orthogonal-factorization-systems.types-local-at-maps + open import synthetic-homotopy-theory.pushouts ``` @@ -37,13 +44,9 @@ Goals Formalize -- is-segal - comp-is-segal - witness-comp-is-segal - uniqueness-comp-is-segal -- is-local-horn-inclusion -- The equivalence between is-local-horn-inclusion and is-segal -- is-local-horn-inclusion-function-type - is-segal-function-type - trivial identities - associativity of comp-is-segal @@ -65,17 +68,17 @@ module simplex cons-Δ : {n : ℕ} (x : Δ n) (i : type-Bounded-Total-Order I) → - (H : leq-Bounded-Total-Order I i (final-Δ n x)) → Δ (succ-ℕ n) + (H : leq-Bounded-Total-Order I i (final-Δ x)) → Δ (succ-ℕ n) - final-Δ : (n : ℕ) → Δ n → type-Bounded-Total-Order I - final-Δ n pt-Δ = top-Bounded-Total-Order I - final-Δ _ (cons-Δ x i H) = i + final-Δ : {n : ℕ} → Δ n → type-Bounded-Total-Order I + final-Δ pt-Δ = top-Bounded-Total-Order I + final-Δ (cons-Δ x i H) = i ap-cons-Δ : {n : ℕ} {x y : Δ n} (p : x ＝ y) {i j : type-Bounded-Total-Order I} (q : i ＝ j) → - (H : leq-Bounded-Total-Order I i (final-Δ n x)) → - (K : leq-Bounded-Total-Order I j (final-Δ n y)) → + (H : leq-Bounded-Total-Order I i (final-Δ x)) → + (K : leq-Bounded-Total-Order I j (final-Δ y)) → cons-Δ x i H ＝ cons-Δ y j K ap-cons-Δ refl refl H K = ap (cons-Δ _ _) (eq-is-prop (is-prop-leq-Bounded-Total-Order I _ _)) @@ -91,8 +94,8 @@ module simplex Eq-cons-Δ : {n : ℕ} {x y : Δ n} {i j : type-Bounded-Total-Order I} → - (H : leq-Bounded-Total-Order I i (final-Δ n x)) → - (K : leq-Bounded-Total-Order I j (final-Δ n y)) → + (H : leq-Bounded-Total-Order I i (final-Δ x)) → + (K : leq-Bounded-Total-Order I j (final-Δ y)) → Eq-Δ n x y → i ＝ j → Eq-Δ (succ-ℕ n) (cons-Δ x i H) (cons-Δ y j K) refl-Eq-Δ : @@ -114,6 +117,20 @@ module simplex in-Δ : type-Bounded-Total-Order I → Δ 1 in-Δ i = cons-Δ pt-Δ i (is-top-element-top-Bounded-Total-Order I _) + is-section-in-Δ : is-section final-Δ in-Δ + is-section-in-Δ i = refl + + is-retraction-in-Δ : is-retraction final-Δ in-Δ + is-retraction-in-Δ (cons-Δ pt-Δ i H) = + ap-cons-Δ refl refl _ H + + is-equiv-in-Δ : is-equiv (final-Δ {1}) + is-equiv-in-Δ = + is-equiv-is-invertible + in-Δ + is-section-in-Δ + is-retraction-in-Δ + d00 : Δ 0 → Δ 1 d00 pt-Δ = in-Δ (top-Bounded-Total-Order I) @@ -125,7 +142,7 @@ module simplex cons-Δ (d00 pt-Δ) i H d11 : Δ 1 → Δ 2 - d11 x = cons-Δ x (final-Δ 1 x) (refl-leq-Bounded-Total-Order I _) + d11 x = cons-Δ x (final-Δ x) (refl-leq-Bounded-Total-Order I _) d12 : Δ 1 → Δ 2 d12 x = @@ -162,11 +179,11 @@ module simplex identity-s00-s10 (cons-Δ x i H) = refl module _ - {l : Level} (X : UU l) + {l : Level} (A : UU l) where nerve-Δ : ℕ → UU (l1 ⊔ l) - nerve-Δ n = Δ n → X + nerve-Δ n = Δ n → A obj-Δ : UU (l1 ⊔ l) obj-Δ = nerve-Δ 0 @@ -174,37 +191,118 @@ module simplex mor-Δ : UU (l1 ⊔ l) mor-Δ = nerve-Δ 1 - dom-Δ : mor-Δ → obj-Δ + module _ + {l : Level} {A : UU l} + where + + dom-Δ : mor-Δ A → obj-Δ A dom-Δ f = f ∘ d01 - cod-Δ : mor-Δ → obj-Δ + cod-Δ : mor-Δ A → obj-Δ A cod-Δ f = f ∘ d00 - id-mor-Δ : obj-Δ → mor-Δ + id-mor-Δ : obj-Δ A → mor-Δ A id-mor-Δ f = f ∘ s00 - + + module _ + {l2 : Level} {A : UU l2} + where + + record + hom-Δ (x y : obj-Δ A) : UU (l1 ⊔ l2) + where + + field + mor-hom-Δ : mor-Δ A + htpy-dom-hom-Δ : dom-Δ mor-hom-Δ ~ x + htpy-cod-hom-Δ : cod-Δ mor-hom-Δ ~ y + + open hom-Δ public + + id-Δ : (x : obj-Δ A) → hom-Δ x x + mor-hom-Δ (id-Δ x) = x ∘ s00 + htpy-dom-hom-Δ (id-Δ x) pt-Δ = refl + htpy-cod-hom-Δ (id-Δ x) pt-Δ = refl + record - midhorn {l : Level} (X : UU l) : UU (l1 ⊔ l) + midhorn {l : Level} (A : UU l) : UU (l1 ⊔ l) where constructor tim field - fstmor sndmor : mor-Δ X - compat : cod-Δ X fstmor pt-Δ ＝ dom-Δ X sndmor pt-Δ + fstmor sndmor : mor-Δ A + compat : cod-Δ fstmor pt-Δ ＝ dom-Δ sndmor pt-Δ representing-midhorn : UU l1 representing-midhorn = pushout d00 d01 + horn-inclusion : representing-midhorn → Δ 2 + horn-inclusion = + cogap d00 d01 (d12 , d10 , inv ∘ identity-d10-d01) + + is-local-horn-inclusion : {l : Level} (A : UU l) → UU (l1 ⊔ l) + is-local-horn-inclusion = is-local horn-inclusion + + is-segal : {l : Level} (A : UU l) → UU (l1 ⊔ l) + is-segal A = + (h : representing-midhorn → A) → is-contr (extension horn-inclusion h) + + module _ + {l : Level} {A : UU l} + where + + is-segal-is-local-horn-inclusion : + is-local-horn-inclusion A → is-segal A + is-segal-is-local-horn-inclusion = + is-contr-extension-is-local horn-inclusion + + is-local-horn-inclusion-is-segal : + is-segal A → is-local-horn-inclusion A + is-local-horn-inclusion-is-segal = + is-local-is-contr-extension horn-inclusion + + module _ + {l2 l3 : Level} {X : UU l2} (A : X → UU l3) + where + + distributive-Π-is-local-horn-inclusion : + ((x : X) → is-local-horn-inclusion (A x)) → + is-local-horn-inclusion ((x : X) → A x) + distributive-Π-is-local-horn-inclusion = + distributive-Π-is-local horn-inclusion A + + distributive-Π-is-segal : + ((x : X) → is-segal (A x)) → is-segal ((x : X) → A x) + distributive-Π-is-segal H = + is-segal-is-local-horn-inclusion + ( distributive-Π-is-local-horn-inclusion + ( λ x → is-local-horn-inclusion-is-segal (H x))) + + module _ + {l2 : Level} {A : UU l2} (H : is-segal A) + where + + horn-composable-hom-Δ : + {x y z : obj-Δ A} → hom-Δ y z → hom-Δ x y → representing-midhorn → A + horn-composable-hom-Δ g f = + cogap d00 d01 + ( mor-hom-Δ f , + mor-hom-Δ g , + ( λ u → htpy-cod-hom-Δ f u ∙ inv (htpy-dom-hom-Δ g u))) + + comp-is-segal : {x y z : obj-Δ A} → hom-Δ y z → hom-Δ x y → hom-Δ x z + mor-hom-Δ (comp-is-segal g f) = + pr1 (center (H (horn-composable-hom-Δ g f))) ∘ d11 + htpy-dom-hom-Δ (comp-is-segal g f) u = {!!} + htpy-cod-hom-Δ (comp-is-segal g f) = {!!} + open midhorn public resmid-Δ : {l : Level} {X : UU l} → nerve-Δ X 2 → midhorn X fstmor (resmid-Δ f) = f ∘ d12 sndmor (resmid-Δ f) = f ∘ d10 compat (resmid-Δ f) = ap f (inv (identity-d10-d01 pt-Δ)) - - is-segal : {l : Level} (X : UU l) → UU (l1 ⊔ l) - is-segal X = is-equiv (resmid-Δ {X = X}) ``` From 81653c691dc9046d3f817934646068b5c20f8999 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Mon, 5 May 2025 17:10:19 -0400 Subject: [PATCH 6/6] work --- .../order-preserving-maps-posets.lagda.md | 47 +++++++ .../order-preserving-maps-preorders.lagda.md | 38 ++++++ src/simplicial-type-theory/simplices.lagda.md | 128 +++++++++++++++++- 3 files changed, 210 insertions(+), 3 deletions(-) diff --git a/src/order-theory/order-preserving-maps-posets.lagda.md b/src/order-theory/order-preserving-maps-posets.lagda.md index 163aee3f3f..2647bc859f 100644 --- a/src/order-theory/order-preserving-maps-posets.lagda.md +++ b/src/order-theory/order-preserving-maps-posets.lagda.md @@ -7,6 +7,8 @@ module order-theory.order-preserving-maps-posets where
Imports ```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.identity-types @@ -19,6 +21,7 @@ open import foundation.universe-levels open import order-theory.order-preserving-maps-preorders open import order-theory.posets +open import order-theory.preorders ```
@@ -209,3 +212,47 @@ module _ ( preorder-Poset R) ( preorder-Poset S) ``` + +### Pointwise inequality of order preserving maps + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4) + where + + leq-hom-Poset : (f g : hom-Poset P Q) → UU (l1 ⊔ l4) + leq-hom-Poset = + leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q) + + is-prop-leq-hom-Poset : + (f g : hom-Poset P Q) → is-prop (leq-hom-Poset f g) + is-prop-leq-hom-Poset = + is-prop-leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q) + + leq-prop-hom-Poset : + (f g : hom-Poset P Q) → Prop (l1 ⊔ l4) + leq-prop-hom-Poset = + leq-prop-hom-Preorder (preorder-Poset P) (preorder-Poset Q) + + refl-leq-hom-Poset : is-reflexive leq-hom-Poset + refl-leq-hom-Poset = + refl-leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q) + + transitive-leq-hom-Poset : + is-transitive leq-hom-Poset + transitive-leq-hom-Poset = + transitive-leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q) + + antisymmetric-leq-hom-Poset : + is-antisymmetric leq-hom-Poset + antisymmetric-leq-hom-Poset f g H K = + eq-htpy-hom-Poset P Q f g (λ x → antisymmetric-leq-Poset Q _ _ (H x) (K x)) + + hom-preorder-Poset : Preorder (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4) + hom-preorder-Poset = + hom-preorder-Preorder (preorder-Poset P) (preorder-Poset Q) + + hom-poset-Poset : Poset (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4) + pr1 hom-poset-Poset = hom-preorder-Poset + pr2 hom-poset-Poset = antisymmetric-leq-hom-Poset +``` diff --git a/src/order-theory/order-preserving-maps-preorders.lagda.md b/src/order-theory/order-preserving-maps-preorders.lagda.md index a45df09656..3c45618541 100644 --- a/src/order-theory/order-preserving-maps-preorders.lagda.md +++ b/src/order-theory/order-preserving-maps-preorders.lagda.md @@ -231,3 +231,41 @@ module _ involutive-eq-associative-comp-hom-Preorder = involutive-eq-eq associative-comp-hom-Preorder ``` + +### Pointwise inequality of order preserving maps + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4) + where + + leq-hom-Preorder : (f g : hom-Preorder P Q) → UU (l1 ⊔ l4) + leq-hom-Preorder f g = + (x : type-Preorder P) → + leq-Preorder Q (map-hom-Preorder P Q f x) (map-hom-Preorder P Q g x) + + is-prop-leq-hom-Preorder : + (f g : hom-Preorder P Q) → is-prop (leq-hom-Preorder f g) + is-prop-leq-hom-Preorder f g = + is-prop-Π (λ x → is-prop-leq-Preorder Q _ _) + + leq-prop-hom-Preorder : + (f g : hom-Preorder P Q) → Prop (l1 ⊔ l4) + pr1 (leq-prop-hom-Preorder f g) = leq-hom-Preorder f g + pr2 (leq-prop-hom-Preorder f g) = is-prop-leq-hom-Preorder f g + + refl-leq-hom-Preorder : (f : hom-Preorder P Q) → leq-hom-Preorder f f + refl-leq-hom-Preorder f x = refl-leq-Preorder Q (map-hom-Preorder P Q f x) + + transitive-leq-hom-Preorder : + (f g h : hom-Preorder P Q) → + leq-hom-Preorder g h → leq-hom-Preorder f g → leq-hom-Preorder f h + transitive-leq-hom-Preorder f g h H K x = + transitive-leq-Preorder Q _ _ _ (H x) (K x) + + hom-preorder-Preorder : Preorder (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4) + pr1 hom-preorder-Preorder = hom-Preorder P Q + pr1 (pr2 hom-preorder-Preorder) = leq-prop-hom-Preorder + pr1 (pr2 (pr2 hom-preorder-Preorder)) = refl-leq-hom-Preorder + pr2 (pr2 (pr2 hom-preorder-Preorder)) = transitive-leq-hom-Preorder +``` diff --git a/src/simplicial-type-theory/simplices.lagda.md b/src/simplicial-type-theory/simplices.lagda.md index e1dee4d113..bd77eadc00 100644 --- a/src/simplicial-type-theory/simplices.lagda.md +++ b/src/simplicial-type-theory/simplices.lagda.md @@ -27,8 +27,12 @@ open import foundation.sections open import foundation.subtypes open import foundation.unit-type open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition open import order-theory.bounded-total-orders +open import order-theory.order-preserving-maps-posets +open import order-theory.posets +open import order-theory.preorders open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.types-local-at-maps @@ -74,6 +78,53 @@ module simplex final-Δ pt-Δ = top-Bounded-Total-Order I final-Δ (cons-Δ x i H) = i + data + functional-Δ-0 : UU l1 + where + pt-functional-Δ-0 : functional-Δ-0 + + is-contr-functional-Δ-0 : is-contr functional-Δ-0 + pr1 is-contr-functional-Δ-0 = pt-functional-Δ-0 + pr2 is-contr-functional-Δ-0 pt-functional-Δ-0 = refl + + leq-functional-Δ-0 : functional-Δ-0 → functional-Δ-0 → UU l1 + leq-functional-Δ-0 x y = functional-Δ-0 + + leq-prop-functional-Δ-0 : + functional-Δ-0 → functional-Δ-0 → Prop l1 + pr1 (leq-prop-functional-Δ-0 x y) = leq-functional-Δ-0 x y + pr2 (leq-prop-functional-Δ-0 x y) = is-prop-is-contr is-contr-functional-Δ-0 + + refl-leq-functional-Δ-0 : is-reflexive leq-functional-Δ-0 + refl-leq-functional-Δ-0 x = pt-functional-Δ-0 + + transitive-leq-functional-Δ-0 : is-transitive leq-functional-Δ-0 + transitive-leq-functional-Δ-0 x y z H K = pt-functional-Δ-0 + + antisymmetric-leq-functional-Δ-0 : is-antisymmetric leq-functional-Δ-0 + antisymmetric-leq-functional-Δ-0 + pt-functional-Δ-0 pt-functional-Δ-0 pt-functional-Δ-0 pt-functional-Δ-0 = + refl + + functional-Δ-0-Preorder : Preorder l1 l1 + pr1 functional-Δ-0-Preorder = functional-Δ-0 + pr1 (pr2 functional-Δ-0-Preorder) = leq-prop-functional-Δ-0 + pr1 (pr2 (pr2 functional-Δ-0-Preorder)) = refl-leq-functional-Δ-0 + pr2 (pr2 (pr2 functional-Δ-0-Preorder)) = transitive-leq-functional-Δ-0 + + functional-Δ-0-Poset : Poset l1 l1 + pr1 functional-Δ-0-Poset = functional-Δ-0-Preorder + pr2 functional-Δ-0-Poset = antisymmetric-leq-functional-Δ-0 + + functional-Δ-Poset : ℕ → Poset l1 l1 + functional-Δ-Poset zero-ℕ = + functional-Δ-0-Poset + functional-Δ-Poset (succ-ℕ n) = + hom-poset-Poset (functional-Δ-Poset n) (poset-Bounded-Total-Order I) + + functional-Δ : ℕ → UU l1 + functional-Δ n = type-Poset (functional-Δ-Poset n) + ap-cons-Δ : {n : ℕ} {x y : Δ n} (p : x ＝ y) {i j : type-Bounded-Total-Order I} (q : i ＝ j) → @@ -239,10 +290,26 @@ module simplex representing-midhorn = pushout d00 d01 + inl-representing-midhorn : Δ 1 → representing-midhorn + inl-representing-midhorn = inl-pushout d00 d01 + + inr-representing-midhorn : Δ 1 → representing-midhorn + inr-representing-midhorn = inr-pushout d00 d01 + horn-inclusion : representing-midhorn → Δ 2 horn-inclusion = cogap d00 d01 (d12 , d10 , inv ∘ identity-d10-d01) + compute-inl-horn-inclusion : + horn-inclusion ∘ inl-representing-midhorn ~ d12 + compute-inl-horn-inclusion = + compute-inl-cogap d00 d01 (d12 , d10 , inv ∘ identity-d10-d01) + + compute-inr-horn-inclusion : + horn-inclusion ∘ inr-representing-midhorn ~ d10 + compute-inr-horn-inclusion = + compute-inr-cogap d00 d01 (d12 , d10 , inv ∘ identity-d10-d01) + is-local-horn-inclusion : {l : Level} (A : UU l) → UU (l1 ⊔ l) is-local-horn-inclusion = is-local horn-inclusion @@ -250,6 +317,22 @@ module simplex is-segal A = (h : representing-midhorn → A) → is-contr (extension horn-inclusion h) + extension-is-segal : + {l : Level} {A : UU l} (H : is-segal A) + (h : representing-midhorn → A) → extension horn-inclusion h + extension-is-segal H h = center (H h) + + 2-simplex-is-segal : + {l : Level} {A : UU l} (H : is-segal A) → + (h : representing-midhorn → A) → Δ 2 → A + 2-simplex-is-segal H h = map-extension (extension-is-segal H h) + + htpy-2-simplex-is-segal : + {l : Level} {A : UU l} (H : is-segal A) → + (h : representing-midhorn → A) → h ~ 2-simplex-is-segal H h ∘ horn-inclusion + htpy-2-simplex-is-segal H h = + is-extension-map-extension (extension-is-segal H h) + module _ {l : Level} {A : UU l} where @@ -292,12 +375,51 @@ module simplex ( mor-hom-Δ f , mor-hom-Δ g , ( λ u → htpy-cod-hom-Δ f u ∙ inv (htpy-dom-hom-Δ g u))) + + compute-inl-horn-composable-hom-Δ : + {x y z : obj-Δ A} (g : hom-Δ y z) (f : hom-Δ x y) → + horn-composable-hom-Δ g f ∘ inl-representing-midhorn ~ mor-hom-Δ f + compute-inl-horn-composable-hom-Δ g f = + compute-inl-cogap + d00 d01 + ( mor-hom-Δ f , + mor-hom-Δ g , + ( λ u → htpy-cod-hom-Δ f u ∙ inv (htpy-dom-hom-Δ g u))) + + compute-inr-horn-composable-hom-Δ : + {x y z : obj-Δ A} (g : hom-Δ y z) (f : hom-Δ x y) → + horn-composable-hom-Δ g f ∘ inr-representing-midhorn ~ mor-hom-Δ g + compute-inr-horn-composable-hom-Δ g f = + compute-inr-cogap + d00 d01 + ( mor-hom-Δ f , + mor-hom-Δ g , + ( λ u → htpy-cod-hom-Δ f u ∙ inv (htpy-dom-hom-Δ g u))) comp-is-segal : {x y z : obj-Δ A} → hom-Δ y z → hom-Δ x y → hom-Δ x z mor-hom-Δ (comp-is-segal g f) = - pr1 (center (H (horn-composable-hom-Δ g f))) ∘ d11 - htpy-dom-hom-Δ (comp-is-segal g f) u = {!!} - htpy-cod-hom-Δ (comp-is-segal g f) = {!!} + 2-simplex-is-segal H (horn-composable-hom-Δ g f) ∘ d11 + htpy-dom-hom-Δ (comp-is-segal {x} {y} {z} g f) = + ( 2-simplex-is-segal H (horn-composable-hom-Δ g f) ·l identity-d11-d01) ∙h + ( inv-htpy + ( 2-simplex-is-segal H (horn-composable-hom-Δ g f) ·l + compute-inl-horn-inclusion ·r d01)) ∙h + ( inv-htpy + ( htpy-2-simplex-is-segal H (horn-composable-hom-Δ g f) ·r + inl-representing-midhorn ∘ d01)) ∙h + ( compute-inl-horn-composable-hom-Δ g f ·r d01) ∙h + ( htpy-dom-hom-Δ f) + htpy-cod-hom-Δ (comp-is-segal g f) = + ( 2-simplex-is-segal H (horn-composable-hom-Δ g f) ·l + inv-htpy identity-d10-d00) ∙h + ( inv-htpy + ( 2-simplex-is-segal H (horn-composable-hom-Δ g f) ·l + compute-inr-horn-inclusion ·r d00)) ∙h + ( inv-htpy + ( htpy-2-simplex-is-segal H (horn-composable-hom-Δ g f) ·r + inr-representing-midhorn ∘ d00)) ∙h + ( compute-inr-horn-composable-hom-Δ g f ·r d00) ∙h + ( htpy-cod-hom-Δ g) open midhorn public