diff --git a/src/Cat/Allegory/Instances/Mat.lagda.md b/src/Cat/Allegory/Instances/Mat.lagda.md index 41afaf64f..5922c2769 100644 --- a/src/Cat/Allegory/Instances/Mat.lagda.md +++ b/src/Cat/Allegory/Instances/Mat.lagda.md @@ -3,6 +3,7 @@ open import Cat.Allegory.Base open import Cat.Prelude +open import Order.Base open import Order.Frame import Order.Frame.Reasoning @@ -25,8 +26,8 @@ are given by $A \times B$-matrices valued in $L$. @@ -69,7 +70,7 @@ the equivalence $(x \le_f y) \equiv (x \le_{\id} f^*y)$ of maps into a [[Cartesian lift]] of the codomain. ```agda - disp : Displayed (Sets ℓ) (o ⊔ ℓ) (o ⊔ ℓ) + disp : Displayed (Sets κ) (o ⊔ κ) (ℓ ⊔ κ) disp .Ob[_] S = ⌞ S ⌟ → ⌞ F ⌟ disp .Hom[_] f g h = ∀ x → g x F.≤ h (f x) disp .Hom[_]-set f g h = is-prop→is-set isp @@ -92,11 +93,11 @@ function $x \mapsto f(x) \cap g(x)$, and the terminal object is the function which is constantly the top element. ```agda - prod : ∀ {S : Set ℓ} (f g : ⌞ S ⌟ → ⌞ F ⌟) → Product (Fibre disp S) f g + prod : ∀ {S : Set κ} (f g : ⌞ S ⌟ → ⌞ F ⌟) → Product (Fibre disp S) f g prod f g .apex x = f x F.∩ g x - prod f g .π₁ i = F.∩≤l - prod f g .π₂ i = F.∩≤r - prod f g .has-is-product .⟨_,_⟩ α β i = F.∩-univ _ (α i) (β i) + prod f g .π₁ i = F.∩-≤l + prod f g .π₂ i = F.∩-≤r + prod f g .has-is-product .⟨_,_⟩ α β i = F.∩-universal _ (α i) (β i) ``` ```agda -module Order.Frame.Reasoning {ℓ} (B : Frame ℓ) where +module Order.Frame.Reasoning {o ℓ} (B : Frame o ℓ) where ``` +```agda +open Frame B public +``` + + # Reasoning about frames This module exposes tools to think about frames as semilattices (their @@ -22,105 +27,93 @@ given by the meet ordering of its finite meets, i.e. $x \le y$ in the frame $B$ iff $x = x \cap y$. ```agda -meets : Semilattice ℓ -meets .fst = B .fst -meets .snd .Semilattice-on.top = _ -meets .snd .Semilattice-on._∩_ = _ -meets .snd .Semilattice-on.has-is-semilattice = Frame-on.has-meets (B .snd) - -open Semilattice meets public -open Frame-on (B .snd) using (⋃ ; ⋃-universal ; ⋃-colimiting ; ⋃-distrib) public +meets : Meet-semilattice o ℓ +meets = B .fst , has-meet-slat + +joins : Join-semilattice o ℓ +joins = B .fst , has-join-slat ``` Using this ordering, we can show that the underlying poset of a frame is indeed cocomplete: -```agda -cocomplete : ∀ {I : Type ℓ} (F : I → ⌞ B ⌟) → Σ _ (is-lub po F) -cocomplete F .fst = ⋃ F -cocomplete F .snd .is-lub.fam≤lub i = ⋃-colimiting i F -cocomplete F .snd .is-lub.least ub' fam≤ub' = ⋃-universal F fam≤ub' -``` - This module also has further lemmas about the interplay between meets and arbitrary joins. The following result holds in any cocomplete lattice: ```agda ⋃-product - : ∀ {I J : Type ℓ} (F : I → ⌞ B ⌟) (G : J → ⌞ B ⌟) + : ∀ {I J : Type o} (F : I → ⌞ B ⌟) (G : J → ⌞ B ⌟) → ⋃ (λ i → ⋃ λ j → G i ∩ F j) ≡ ⋃ {I = I × J} (λ p → F (p .fst) ∩ G (p .snd)) -⋃-product {I} {J} F G = ≤-antisym - (⋃-universal _ λ j → ⋃-universal _ λ i → - G j ∩ F i =⟨ ∩-commutative ⟩ - F i ∩ G j ≤⟨ ⋃-colimiting (i , j) _ ⟩ - ⋃ {I = I × J} (λ v → F (v .fst) ∩ G (v .snd)) ≤∎) - (⋃-universal _ λ { (i , j) → - F i ∩ G j ≤⟨ ⋃-colimiting i (λ i → F i ∩ G j) ⟩ - ⋃ (λ i → F i ∩ G j) ≤⟨ ⋃-colimiting j (λ j → ⋃ λ i → F i ∩ G j) ⟩ - ⋃ (λ i → ⋃ λ j → F j ∩ G i) =⟨ ap ⋃ (funext λ i → ap ⋃ $ funext λ j → ∩-commutative) ⟩ - ⋃ (λ i → ⋃ λ j → G i ∩ F j) ≤∎ }) +⋃-product {I} {J} F G = + ≤-antisym + (⋃-universal _ λ j → ⋃-universal _ λ i → + G j ∩ F i =⟨ ∩-comm _ _ ⟩ + F i ∩ G j ≤⟨ fam≤⋃ (i , j) ⟩ + ⋃ {I = I × J} (λ v → F (v .fst) ∩ G (v .snd)) ≤∎) + (⋃-universal _ λ where + (i , j) → + F i ∩ G j ≤⟨ fam≤⋃ i ⟩ + ⋃ (λ i → F i ∩ G j) ≤⟨ fam≤⋃ j ⟩ + ⋃ (λ i → ⋃ λ j → F j ∩ G i) =⟨ ap ⋃ (funext λ i → ap ⋃ $ funext λ j → ∩-comm (F j) (G i)) ⟩ + ⋃ (λ i → ⋃ λ j → G i ∩ F j) ≤∎) ``` But this result relies on the cocontinuity of meets. ```agda ⋃-∩-product - : ∀ {I J : Type ℓ} (F : I → ⌞ B ⌟) (G : J → ⌞ B ⌟) + : ∀ {I J : Type o} (F : I → ⌞ B ⌟) (G : J → ⌞ B ⌟) → ⋃ F ∩ ⋃ G ≡ ⋃ {I = I × J} (λ i → F (i .fst) ∩ G (i .snd)) ⋃-∩-product F G = - ⋃ F ∩ ⋃ G ≡⟨ ⋃-distrib (⋃ F) G ⟩ - ⋃ (λ i → ⋃ F ∩ G i) ≡⟨ ap ⋃ (funext λ i → ∩-commutative ∙ ⋃-distrib (G i) F) ⟩ + ⋃ F ∩ ⋃ G ≡⟨ ⋃-distribl (⋃ F) G ⟩ + ⋃ (λ i → ⋃ F ∩ G i) ≡⟨ ap ⋃ (funext λ i → ∩-comm _ _ ∙ ⋃-distribl (G i) F) ⟩ ⋃ (λ i → ⋃ λ j → G i ∩ F j) ≡⟨ ⋃-product F G ⟩ ⋃ (λ i → F (i .fst) ∩ G (i .snd)) ∎ ⋃-twice - : ∀ {I : Type ℓ} {J : I → Type ℓ} (F : (i : I) → J i → ⌞ B ⌟) + : ∀ {I : Type o} {J : I → Type o} (F : (i : I) → J i → ⌞ B ⌟) → ⋃ (λ i → ⋃ λ j → F i j) ≡ ⋃ {I = Σ I J} (λ p → F (p .fst) (p .snd)) ⋃-twice F = ≤-antisym - (⋃-universal _ (λ i → ⋃-universal _ (λ j → ⋃-colimiting _ _))) - (⋃-universal _ λ (i , j) → ≤-trans (⋃-colimiting j _) (⋃-colimiting i _)) + (⋃-universal _ (λ i → ⋃-universal _ (λ j → fam≤⋃ _))) + (⋃-universal _ λ (i , j) → ≤-trans (fam≤⋃ j) (fam≤⋃ i)) ⋃-ap - : ∀ {I I' : Type ℓ} {f : I → ⌞ B ⌟} {g : I' → ⌞ B ⌟} + : ∀ {I I' : Type o} {f : I → ⌞ B ⌟} {g : I' → ⌞ B ⌟} → (e : I ≃ I') → (∀ i → f i ≡ g (e .fst i)) → ⋃ f ≡ ⋃ g ⋃-ap e p = ap₂ (λ I f → ⋃ {I = I} f) (ua e) (ua→ p) -- raised i for "index", raised f for "family" -⋃-apⁱ : ∀ {I I' : Type ℓ} {f : I' → ⌞ B ⌟} (e : I ≃ I') → ⋃ (λ i → f (e .fst i)) ≡ ⋃ f -⋃-apᶠ : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟} → (∀ i → f i ≡ g i) → ⋃ f ≡ ⋃ g +⋃-apⁱ : ∀ {I I' : Type o} {f : I' → ⌞ B ⌟} (e : I ≃ I') → ⋃ (λ i → f (e .fst i)) ≡ ⋃ f +⋃-apᶠ : ∀ {I : Type o} {f g : I → ⌞ B ⌟} → (∀ i → f i ≡ g i) → ⋃ f ≡ ⋃ g ⋃-apⁱ e = ⋃-ap e (λ i → refl) ⋃-apᶠ p = ⋃-ap (_ , id-equiv) p ⋃-singleton - : ∀ {I : Type ℓ} {f : I → ⌞ B ⌟} + : ∀ {I : Type o} {f : I → ⌞ B ⌟} → (p : is-contr I) → ⋃ f ≡ f (p .centre) ⋃-singleton {f = f} p = ≤-antisym - (⋃-universal _ (λ i → sym ∩-idempotent ∙ ap₂ _∩_ refl (ap f (sym (p .paths _))))) - (⋃-colimiting _ _) - -⋃-distribʳ - : ∀ {I : Type ℓ} {f : I → ⌞ B ⌟} {x} - → ⋃ f ∩ x ≡ ⋃ (λ i → f i ∩ x) -⋃-distribʳ = ∩-commutative ∙ ⋃-distrib _ _ ∙ ap ⋃ (funext λ _ → ∩-commutative) + (⋃-universal _ λ i → path→≥ $ ap f (p .paths i)) + (fam≤⋃ _) ⋃≤⋃ - : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟} + : ∀ {I : Type o} {f g : I → ⌞ B ⌟} → (∀ i → f i ≤ g i) → ⋃ f ≤ ⋃ g -⋃≤⋃ p = ⋃-universal _ (λ i → ≤-trans (p i) (⋃-colimiting _ _)) +⋃≤⋃ p = ⋃-universal _ (λ i → ≤-trans (p i) (fam≤⋃ _)) +-- FIXME: this ought to live somewhere else ∩≤∩ : ∀ {x y x' y'} → x ≤ x' → y ≤ y' → (x ∩ y) ≤ (x' ∩ y') -∩≤∩ p q = ∩-univ _ (≤-trans ∩≤l p) (≤-trans ∩≤r q) +∩≤∩ p q = ∩-universal _ (≤-trans ∩-≤l p) (≤-trans ∩-≤r q) ``` diff --git a/src/Order/Semilattice.lagda.md b/src/Order/Semilattice.lagda.md index 86f2ceeda..4a4e89897 100644 --- a/src/Order/Semilattice.lagda.md +++ b/src/Order/Semilattice.lagda.md @@ -395,10 +395,23 @@ Join-slat-subcat o ℓ .Subcat.is-hom-prop = hlevel! Join-slat-subcat o ℓ .Subcat.is-hom-id = id-join-slat-hom Join-slat-subcat o ℓ .Subcat.is-hom-∘ = ∘-join-slat-hom -Meet-slat : ∀ o ℓ → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ) -Meet-slat o ℓ = Subcategory (Meet-slat-subcat o ℓ) +Meet-slats : ∀ o ℓ → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ) +Meet-slats o ℓ = Subcategory (Meet-slat-subcat o ℓ) -Join-slat : ∀ o ℓ → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ) -Join-slat o ℓ = Subcategory (Join-slat-subcat o ℓ) +Join-slats : ∀ o ℓ → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ) +Join-slats o ℓ = Subcategory (Join-slat-subcat o ℓ) +``` + +```agda +module Meet-slats {o} {ℓ} = Cat.Reasoning (Meet-slats o ℓ) +module Join-slats {o} {ℓ} = Cat.Reasoning (Join-slats o ℓ) +``` + +```agda +Meet-semilattice : ∀ o ℓ → Type _ +Meet-semilattice o ℓ = Meet-slats.Ob {o} {ℓ} + +Join-semilattice : ∀ o ℓ → Type _ +Join-semilattice o ℓ = Join-slats.Ob {o} {ℓ} ``` diff --git a/src/Order/Semilattice/Order.lagda.md b/src/Order/Semilattice/Order.lagda.md deleted file mode 100644 index ab5827ba4..000000000 --- a/src/Order/Semilattice/Order.lagda.md +++ /dev/null @@ -1,83 +0,0 @@ - - -```agda -module Order.Semilattice.Order where -``` - -# Semilattices from posets - -We have already established that [[semilattices]], which we define -algebraically, have an underlying [[poset]]. The aim of this module is to -prove the converse: If you have a poset $(A, \le)$ such that any finite -number of elements has a greatest lower bound, then $A$ is a -semilattice. As usual, by induction, it suffices to have nullary and -binary greatest lower bounds: A top element, and meets. - -To this end, we define a type of [[finitely complete]] posets: Posets -possessing meets and a top element. - -```agda -record Finitely-complete-poset ℓₒ ℓᵣ : Type (lsuc (ℓₒ ⊔ ℓᵣ)) where - no-eta-equality - field - poset : Poset ℓₒ ℓᵣ - _∩_ : ⌞ poset ⌟ → ⌞ poset ⌟ → ⌞ poset ⌟ - has-is-meet : ∀ {x y} → is-meet poset x y (x ∩ y) - - top : ⌞ poset ⌟ - has-is-top : ∀ {x} → Poset._≤_ poset x top - - open Poset poset public - private module meet {x} {y} = is-meet (has-is-meet {x} {y}) - open meet renaming (meet≤l to ∩≤l ; meet≤r to ∩≤r ; greatest to ∩-univ) public - - le→meet : ∀ {x y} → x ≤ y → x ≡ x ∩ y - le→meet x≤y = le-meet poset x≤y has-is-meet - - meet→le : ∀ {x y} → x ≡ x ∩ y → x ≤ y - meet→le {y = y} x=x∩y = subst (_≤ y) (sym x=x∩y) ∩≤r -``` - -From a finitely complete poset, we can define a semilattice: from the -universal property of meets, we can conclude that they are associative, -idempotent, commutative, and have the top element as a unit. - -```agda -fc-poset→semilattice : ∀ {o ℓ} (P : Finitely-complete-poset o ℓ) → Semilattice o -fc-poset→semilattice P = to-semilattice make-p where - module ml = make-semilattice - open Finitely-complete-poset P - - make-p : make-semilattice ⌞ poset ⌟ - make-p .ml.has-is-set = hlevel! - make-p .ml.top = top - make-p .ml.op = _∩_ - make-p .ml.idl = ≤-antisym ∩≤r (∩-univ _ has-is-top ≤-refl) - make-p .ml.associative = ≤-antisym - (∩-univ _ - (∩-univ _ ∩≤l (≤-trans ∩≤r ∩≤l)) - (≤-trans ∩≤r ∩≤r)) - (∩-univ _ (≤-trans ∩≤l ∩≤l) (∩-univ _ (≤-trans ∩≤l ∩≤r) ∩≤r)) - make-p .ml.commutative = ≤-antisym - (∩-univ _ ∩≤r ∩≤l) - (∩-univ _ ∩≤r ∩≤l) - make-p .ml.idempotent = ≤-antisym ∩≤l (∩-univ _ ≤-refl ≤-refl) -``` - -It's a general fact about meets that the semilattice ordering defined -with the meets from a finitely complete poset agrees with our original -ordering, which we link below: - -```agda -_ = le-meet -```