defn: suplattices, basic covers

src/1Lab/Resizing.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+open import 1Lab.Function.Surjection
 open import 1Lab.Path.IdentitySystem
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Retracts
@@ -266,3 +267,18 @@ These connectives and quantifiers are only provided for completeness;
 if you find yourself building nested propositions, it is generally a good
 idea to construct the large proposition by hand, and then use truncation
 to turn it into a small proposition.
+
+<!--
+```agda
+module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where
+  Ω-image : Type ℓ'
+  Ω-image = Σ[ b ∈ B ] □ (fibre f b)
+
+  Ω-corestriction : A → Ω-image
+  Ω-corestriction a = f a , inc (a , refl)
+
+  opaque
+    Ω-corestriction-is-surjective : is-surjective Ω-corestriction
+    Ω-corestriction-is-surjective (b , p) = □-rec! (λ (a , p) → inc (a , Σ-prop-path! p)) p
+```
+-->

src/Algebra/Group/Subgroup.lagda.md

@@ -27,7 +27,7 @@ private module _ {ℓ} where open Cat.Displayed.Instances.Subobjects (Groups ℓ
 ```
 -->
 
-# Subgroups
+# Subgroups {defines="subgroup"}
 
 A **subgroup** $m$ of a group $G$ is a [[monomorphism]] $H \xto{m} G$,
 that is, an object of the [[poset of subobjects]] $\Sub(G)$. Since group

src/Cat/Allegory/Instances/Mat.lagda.md

@@ -4,6 +4,7 @@ open import Cat.Allegory.Base
 open import Cat.Prelude
 
 open import Order.Frame
+open import Order.Base
 
 import Order.Frame.Reasoning
 ```
@@ -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 .snd)
   open Precategory
   private module A = Allegory
 ```
@@ -56,60 +57,58 @@ that this is, indeed, a category:
   Mat .id x y              = ⋃ λ (_ : x ≡ y) → top
   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)) ⟩
+  Mat .idr M = ext λ i j →
+    ⋃ (λ k → ⋃ (λ _ → top) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ∩-comm ∙ ⋃-distribl _ _) ⟩
+    ⋃ (λ k → ⋃ (λ _ → M k j ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-apᶠ λ 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 _ _) ⟩
+  Mat .idl M = ext λ i j →
+    ⋃ (λ 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ʳ) ⟩
+  Mat .assoc M N O = ext λ i j →
+    ⋃ (λ 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ⁱ ×-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ᶠ (λ k → sym (⋃-distribl _ _)) ⟩
     ⋃ (λ l → O i l ∩ ⋃ (λ k → N l k ∩ M k j))   ∎
 ```
 
 Most of the structure of an allegory now follows directly from the fact
-that frames are also [semilattices]: the ordering, duals, and
+that frames are also [[meet semilattices]]: the ordering, duals, and
 intersections are all computed pointwise. The only thing which requires
 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
 
   Matrices .A.≤-thin          = hlevel!
   Matrices .A.≤-refl i j      = ≤-refl
   Matrices .A.≤-trans p q i j = ≤-trans (p i j) (q i j)
-  Matrices .A.≤-antisym p q   = funext² λ i j → ≤-antisym (p i j) (q i j)
+  Matrices .A.≤-antisym p q   = ext λ i j → ≤-antisym (p i j) (q i j)
   Matrices .A._◆_ p q i j     = ⋃≤⋃ (λ k → ∩≤∩ (q i k) (p k j))
 
   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-∘       = ext λ 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.∩-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 _ (∩≤∩r (⋃-inj j)) (≤-trans ∩≤r ∩≤r)) ⟩
     ⋃ (λ k → (f i k ∩ ⋃ (λ l → h i l ∩ g k l)) ∩ g k j) ≤∎
 ```

src/Cat/Diagram/Monad.lagda.md

@@ -22,7 +22,7 @@ module _ {o h : _} (C : Precategory o h) where
 ```
 -->
 
-# Monads
+# Monads {defines="monad"}
 
 A **monad on a category** $\cC$ is one way of categorifying the
 concept of [monoid]. Specifically, rather than living in a monoidal
@@ -65,7 +65,7 @@ associativity laws exactly analogous to those of a monoid.
       mult-assoc  : ∀ {x} → mult.η x C.∘ M₁ (mult.η x) ≡ mult.η x C.∘ mult.η (M₀ x)
 ```
 
-# Algebras over a monad
+# Algebras over a monad {defines="monad-algebra"}
 
 One way of interpreting a monad $M$ is as giving a _signature_ for an
 algebraic theory. For instance, the [[free monoid]] monad describes the
@@ -118,7 +118,7 @@ doesn't matter whether you first join then evaluate, or evaluate twice.
 ```
 -->
 
-# Eilenberg-Moore category
+# Eilenberg-Moore category {defines="eilenberg-moore-category"}
 
 If we take a monad $M$ as the signature of an (algebraic) theory, and
 $M$-algebras as giving _models_ of that theory, then we can ask (like

src/Cat/Displayed/Doctrine.lagda.md

@@ -236,7 +236,7 @@ is a pullback.
 
 That concludes the definition of regular hyperdoctrine. Said snappily, a
 **regular hyperdoctrine** $\bP \liesover \cB$ is a [[bifibration]] into
-[[(meet-)semilattices|semilattice]] satisfying Frobenius reciprocity and
+[[(meet-)semilattices|meet-semilattice]] satisfying Frobenius reciprocity and
 the Beck-Chevalley condition.
 
 <!--

src/Cat/Displayed/Doctrine/Frame.lagda.md

@@ -12,6 +12,7 @@ open import Cat.Displayed.Base
 open import Cat.Prelude
 
 open import Order.Frame
+open import Order.Base
 
 import Cat.Reasoning as Cat
 
@@ -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
+  module F = Frm (F .snd)
 
   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
 ```
 -->
@@ -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 .has-is-product .⟨_,_⟩ α β i = F.∩-universal _ (α i) (β i)
 ```
 
 <!--
@@ -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
@@ -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.⋃-inj (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 ⟩
@@ -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 _ _))
@@ -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.⋃-inj
           ( 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.⋃-inj (α 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
 ```

src/Data/Fin/Indexed.lagda.md

@@ -131,7 +131,7 @@ T \to \Omega$ is finitely-indexed if its total space $\Sigma_{x : T} x
 \in P$ is. To disambiguate and keep names short, we refer to types as
 finitely-indexed, but to subsets as **K-finite**.
 
-The $K$-finite subsets of $T$ are a sub-join[[semilattice]] of the
+The $K$-finite subsets of $T$ are a sub-[[join semilattice]] of the
 [[power-set]] lattice of $T$. That is, the empty subset is $K$-finite,
 and any union is $K$-finite as well. Since the empty subset is _finite_,
 it's also $K$-finite, of course.
@@ -175,7 +175,7 @@ not an issue here.
         (inr x) → g x .fst , inc (inr (g x .snd))
 
       surj' : ∀ x → ∥ fibre cover' x ∥
-      surj' xf = □-tr (xf .snd) >>= λ where
+      surj' xf = (xf .snd) >>= λ where
         (inl p) → do
           (ix , p) ← f-surj (xf .fst , p)
           pure (inl ix , Σ-prop-path! (ap fst p))
@@ -189,7 +189,7 @@ not an issue here.
 Moreover, we have that a singleton set is $K$-finite, as well.
 
 ```agda
-  singleton-is-K-finite : is-set T → (x : T) → is-K-finite (λ y → elΩ (x ≡ y))
+  singleton-is-K-finite : is-set T → (x : T) → is-K-finite (singleton x)
   singleton-is-K-finite t-set x = inc (cover {cardinality = 1} (λ _ → x , inc refl)
     λ (y , p) → inc (fzero , Σ-prop-path (λ _ → squash) (out! {pa = t-set _ _} p)))
 ```