Skip to content

Commit

Permalink
wip: fix files
Browse files Browse the repository at this point in the history
  • Loading branch information
@TOTBWF
TOTBWF committed Nov 30, 2023
1 parent fdcb5cc commit 977db72
Show file tree
Hide file tree
Showing 5 changed files with 94 additions and 170 deletions.
35 changes: 18 additions & 17 deletions src/Cat/Allegory/Instances/Mat.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -25,8 +26,8 @@ are given by $A \times B$-matrices valued in $L$.

<!--
```agda
module _ (o : Level) (L : Frame o) where
open Order.Frame.Reasoning L hiding (Ob ; Hom-set)
module _ {o ℓ : Level} (L : Frame o ℓ) where
open Order.Frame.Reasoning L
open Precategory
private module A = Allegory
```
Expand Down Expand Up @@ -57,25 +58,25 @@ that this is, indeed, a category:
Mat ._∘_ {y = y} M N i j = ⋃ λ k → N i k ∩ M k j

Mat .idr M = funext² λ i j →
⋃ (λ k → ⋃ (λ _ → top) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ∩-commutative ∙ ⋃-distrib _ _) ⟩
⋃ (λ k → ⋃ (λ _ → M k j ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ap ⋃ (funext λ i → ∩-idr)) ⟩
⋃ (λ k → ⋃ (λ _ → top) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ∩-comm _ _ ∙ ⋃-distribl _ _) ⟩
⋃ (λ k → ⋃ (λ _ → M k j ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ap ⋃ (funext λ i → (∩-idr _))) ⟩
⋃ (λ k → ⋃ (λ _ → M k j)) ≡⟨ ⋃-twice _ ⟩
⋃ (λ (k , _) → M k j) ≡⟨ ⋃-singleton (contr _ Singleton-is-contr) ⟩
M i j ∎
Mat .idl M = funext² λ i j →
⋃ (λ k → M i k ∩ ⋃ (λ _ → top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-distrib _ _) ⟩
⋃ (λ k → ⋃ (λ _ → M i k ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-apᶠ λ j → ∩-idr) ⟩
⋃ (λ k → M i k ∩ ⋃ (λ _ → top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-distribl _ _) ⟩
⋃ (λ k → ⋃ (λ _ → M i k ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-apᶠ λ j → (∩-idr _)) ⟩
⋃ (λ x → ⋃ (λ _ → M i x)) ≡⟨ ⋃-twice _ ⟩
⋃ (λ (k , _) → M i k) ≡⟨ ⋃-singleton (contr _ (λ p i → p .snd (~ i) , λ j → p .snd (~ i ∨ j))) ⟩
M i j ∎

Mat .assoc M N O = funext² λ i j →
⋃ (λ k → ⋃ (λ l → O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ⋃-distribʳ) ⟩
⋃ (λ k → ⋃ (λ l → O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → (⋃-distribr _ _)) ⟩
⋃ (λ k → ⋃ (λ l → (O i l ∩ N l k) ∩ M k j)) ≡⟨ ⋃-twice _ ⟩
⋃ (λ (k , l) → (O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ _ → sym ∩-assoc) ⟩
⋃ (λ (k , l) → (O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ _ → sym (∩-assoc _ _ _)) ⟩
⋃ (λ (k , l) → O i l ∩ (N l k ∩ M k j)) ≡⟨ ⋃-apⁱ ×-swap ⟩
⋃ (λ (l , k) → O i l ∩ (N l k ∩ M k j)) ≡˘⟨ ⋃-twice _ ⟩
⋃ (λ l → ⋃ (λ k → O i l ∩ (N l k ∩ M k j))) ≡⟨ ap ⋃ (funext λ k → sym (⋃-distrib _ _)) ⟩
⋃ (λ l → ⋃ (λ k → O i l ∩ (N l k ∩ M k j))) ≡⟨ ap ⋃ (funext λ k → sym (⋃-distribl _ _)) ⟩
⋃ (λ l → O i l ∩ ⋃ (λ k → N l k ∩ M k j)) ∎
```

Expand All @@ -87,7 +88,7 @@ a bit more algebra is the verification of the modular law:
[semilattices]: Order.Semilattice.html

```agda
Matrices : Allegory (lsuc o) o o
Matrices : Allegory (lsuc o) o (o ⊔ ℓ)
Matrices .A.cat = Mat
Matrices .A._≤_ M N = ∀ i j → M i j ≤ N i j

Expand All @@ -100,16 +101,16 @@ a bit more algebra is the verification of the modular law:
Matrices .A._† M i j = M j i
Matrices .A.dual-≤ x i j = x j i
Matrices .A.dual M = refl
Matrices .A.dual-∘ = funext² λ i j → ⋃-apᶠ λ k → ∩-commutative
Matrices .A.dual-∘ = funext² λ i j → ⋃-apᶠ λ k → ∩-comm _ _

Matrices .A._∩_ M N i j = M i j ∩ N i j
Matrices .A.∩-le-l i j = ∩≤l
Matrices .A.∩-le-r i j = ∩≤r
Matrices .A.∩-univ p q i j = ∩-univ _ (p i j) (q i j)
Matrices .A.∩-le-l i j = ∩-≤l
Matrices .A.∩-le-r i j = ∩-≤r
Matrices .A.∩-univ p q i j = ∩-universal _ (p i j) (q i j)

Matrices .A.modular f g h i j =
⋃ (λ k → f i k ∩ g k j) ∩ h i j =⟨ ⋃-distribʳ ∙ ⋃-apᶠ (λ _ → sym ∩-assoc) ⟩
⋃ (λ k → f i k ∩ (g k j ∩ h i j)) =⟨ ⋃-apᶠ (λ k → ap₂ _∩_ refl ∩-commutative) ⟩
⋃ (λ k → f i k ∩ (h i j ∩ g k j)) ≤⟨ ⋃≤⋃ (λ i → ∩-univ _ (∩-univ _ ∩≤l (≤-trans ∩≤r (⋃-colimiting _ _))) (≤-trans ∩≤r ∩≤r)) ⟩
⋃ (λ k → f i k ∩ g k j) ∩ h i j =⟨ ⋃-distribr _ _ ∙ ⋃-apᶠ (λ _ → sym (∩-assoc _ _ _)) ⟩
⋃ (λ k → f i k ∩ (g k j ∩ h i j)) =⟨ ⋃-apᶠ (λ k → ap₂ _∩_ refl (∩-comm _ _)) ⟩
⋃ (λ k → f i k ∩ (h i j ∩ g k j)) ≤⟨ ⋃≤⋃ (λ i → ∩-universal _ (∩-universal _ ∩-≤l (≤-trans ∩-≤r (fam≤⋃ _))) (≤-trans ∩-≤r ∩-≤r)) ⟩
⋃ (λ k → (f i k ∩ ⋃ (λ l → h i l ∩ g k l)) ∩ g k j) ≤∎
```
38 changes: 19 additions & 19 deletions src/Cat/Displayed/Doctrine/Frame.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

open import Order.Base
open import Order.Frame

import Cat.Reasoning as Cat
Expand Down Expand Up @@ -44,16 +45,16 @@ the Grothendieck construction to $\hom(-,X)$. We will construct this in
very explicit stages.

```agda
Indexed-frame : ∀ {o ℓ} → Frame o → Regular-hyperdoctrine (Sets ℓ) (o ⊔ ℓ) (o ⊔ ℓ)
Indexed-frame {o = o} {ℓ} F = idx where
Indexed-frame : ∀ {o ℓ κ} → Frame o ℓ → Regular-hyperdoctrine (Sets κ) (o ⊔ κ) (ℓ ⊔ κ)
Indexed-frame {o = o} {ℓ} {κ} F = idx where
```

<!--
```agda
module F = Frm F

private opaque
isp : ∀ {x : Type ℓ} {f g : x → ⌞ F ⌟} → is-prop (∀ x → f x F.≤ g x)
isp : ∀ {x : Type κ} {f g : x → ⌞ F ⌟} → is-prop (∀ x → f x F.≤ g x)
isp = Π-is-hlevel 1 λ _ → F.≤-thin
```
-->
Expand All @@ -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
Expand All @@ -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)
```

<!--
Expand All @@ -110,7 +111,7 @@ function which is constantly the top element.
```agda
term : ∀ S → Terminal (Fibre disp S)
term S .top _ = F.top
term S .has⊤ f = is-prop∙→is-contr isp (λ i → sym F.∩-idr)
term S .has⊤ f = is-prop∙→is-contr isp (λ i → F.!)
```

## As a fibration
Expand Down Expand Up @@ -180,8 +181,8 @@ a calculation:
```agda
lifted : Cocartesian-lift disp f g
lifted .y' y = exist y
lifted .lifting i = F.⋃-colimiting (g i , inc (i , refl , refl)) fst
lifted .cocartesian .universal {u' = u'} m h' i = F.⋃-universal fst λ (e , b) →
lifted .lifting i = F.fam≤⋃ (g i , inc (i , refl , refl))
lifted .cocartesian .universal {u' = u'} m h' i = F.⋃-universal _ λ (e , b) →
□-rec! (λ { (x , p , q) →
e F.=⟨ sym q ⟩
g x F.≤⟨ h' x ⟩
Expand All @@ -197,9 +198,9 @@ We're ready to put everything together. By construction, we have a
"category displayed in posets",

```agda
idx : Regular-hyperdoctrine (Sets ℓ) _ _
idx : Regular-hyperdoctrine (Sets κ) _ _
idx .ℙ = disp
idx .has-is-set x = Π-is-hlevel 2 λ _ → F .fst .is-tr
idx .has-is-set x = Π-is-hlevel 2 λ _ → F.Ob-is-set
idx .has-is-thin f g = isp
idx .has-univalence S = set-identity-system
(λ _ _ _ _ → Cat.≅-path (Fibre disp _) (isp _ _))
Expand Down Expand Up @@ -228,22 +229,21 @@ distributive law in $F$:

```agda
idx .frobenius {X} {Y} f {α} {β} = funext λ i → F.≤-antisym
( exist α i F.∩ β i F.=⟨ F.⋃-distribʳ ⟩
( exist α i F.∩ β i F.=⟨ F.⋃-distribr _ _ ⟩
F.⋃ {I = img α i} (λ (x , _) → x F.∩ β i) F.≤⟨
F.⋃-universal _ (λ img → F.⋃-colimiting
F.⋃-universal _ (λ img → F.fam≤⋃

This comment has been minimized.

Sign in to view

Copy link
@plt-amy

plt-amy Nov 30, 2023

Member

Looks like you accidentally fixed the complaint I was going to raise about -universal and -colimiting disagreeing on the order in which they take their arguments (index/family) 🙂
( img .fst F.∩ β i
, □-map (λ { (x , p , q) → x , p , ap₂ F._∩_ q (ap β p) }) (img .snd))
fst)
, □-map (λ { (x , p , q) → x , p , ap₂ F._∩_ q (ap β p) }) (img .snd)))
⟩
exist (λ x → α x F.∩ β (f x)) i F.≤∎ )
( exist (λ x → α x F.∩ β (f x)) i F.≤⟨
F.⋃-universal _ (λ (e , p) → □-rec! (λ { (x , p , q) →
e F.=⟨ sym q ⟩
α x F.∩ β (f x) F.=⟨ ap (α x F.∩_) (ap β p) ⟩
α x F.∩ β i F.≤⟨ F.⋃-colimiting (α x , inc (x , p , refl)) _ ⟩
α x F.∩ β i F.≤⟨ F.fam≤⋃ (α x , inc (x , p , refl)) ⟩
F.⋃ {I = img α i} (λ (x , _) → x F.∩ β i) F.≤∎ }) p)
⟩
F.⋃ {I = img α i} (λ (x , _) → x F.∩ β i) F.=⟨ sym F.⋃-distribʳ ⟩
F.⋃ {I = img α i} (λ (x , _) → x F.∩ β i) F.=⟨ sym (F.⋃-distribr _ _) ⟩
exist α i F.∩ β i F.≤∎)
where open cocart {X} {Y} f
```
Expand Down
87 changes: 40 additions & 47 deletions src/Order/Frame/Reasoning.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,14 @@ open import Order.Base
-->

```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
Expand All @@ -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)
```
21 changes: 17 additions & 4 deletions src/Order/Semilattice.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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} {ℓ}
```

Loading

0 comments on commit 977db72

Please sign in to comment.