Merge branch 'main' into comprehension-coproducts

.github/workflows/build.yml

@@ -32,8 +32,8 @@ jobs:
         uses: actions/cache@v3
         with:
           path: _build
-          key: shake-3-${{ env.shake_version }}-${{ github.run_id }}
-          restore-keys: shake-3-${{ env.shake_version }}-
+          key: shake-4-${{ env.shake_version }}-${{ github.run_id }}
+          restore-keys: shake-4-${{ env.shake_version }}-
 
       - name: Build 🛠️
         run: |

src/1Lab/Reflection.lagda.md

@@ -8,7 +8,7 @@ open import 1Lab.Type hiding (absurd)
 open import Data.Product.NAry
 open import Data.Vec.Base
 open import Data.Bool
-open import Data.List
+open import Data.List.Base
 ```
 -->
 
@@ -27,7 +27,7 @@ open import Meta.Alt public
 
 open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public
 open Data.Product.NAry using ([_]) public
-open Data.List public
+open Data.List.Base public
 open Data.Bool public
 ```
 

src/1Lab/Reflection/HLevel.agda

@@ -10,7 +10,7 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Bool
-open import Data.List
+open import Data.List.Base
 
 open import Meta.Foldable
 
@@ -678,11 +678,6 @@ instance
   decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B)
   decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] )
 
-  -- List isn't really a type on the same footing as all the others, but
-  -- we're here, so we might as well, right?
-  decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A)
-  decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus 2 ∷ `search ∷ [])
-
   -- This one really ought to work with instance selection only, but
   -- Agda has trouble with the (1 + k + n) level in H-Level-n-Type. The
   -- decomposition here is a bit more flexible.

src/1Lab/Reflection/Marker.agda

@@ -3,7 +3,7 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Maybe.Base
-open import Data.List
+open import Data.List.Base
 
 open import Prim.Data.Nat
 

src/1Lab/Reflection/Record.agda

@@ -4,7 +4,6 @@ open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
 
-open import Data.List
 
 import Prim.Data.Sigma as S
 import Prim.Data.Nat as N

src/1Lab/Reflection/Variables.agda

@@ -3,7 +3,7 @@ open import 1Lab.Type
 
 open import Data.Fin.Base
 open import Data.Nat.Base
-open import Data.List hiding (reverse)
+open import Data.List.Base hiding (reverse)
 
 module 1Lab.Reflection.Variables where
 

src/1Lab/Type/Pi.lagda.md

@@ -176,3 +176,14 @@ hetero-homotopy≃homotopy {A = A} {B} {f} {g} = Iso→Equiv isom where
       j
       (h (SinglP-is-contr A x₀ .paths (x₁ , p) j .snd))
 ```
+
+<!--
+```agda
+funext²
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : ∀ x → B x → Type ℓ''}
+      {f g : ∀ x y → C x y}
+  → (∀ i j → f i j ≡ g i j)
+  → f ≡ g
+funext² p i x y = p x y i
+```
+-->

src/1Lab/Type/Sigma.lagda.md

@@ -279,5 +279,12 @@ infixr 4 _,ₚ_
 Σ-swap₂ .snd .is-eqv y = contr (f .fst) (f .snd) where
   f = strict-fibres _ y
   -- agda can actually infer the inverse here, which is neat
+
+×-swap
+  : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′}
+  → (A × B) ≃ (B × A)
+×-swap .fst (x , y) = y , x
+×-swap .snd .is-eqv y = contr (f .fst) (f .snd) where
+  f = strict-fibres _ y
 ```
 -->

src/Algebra/Group/Cat/Base.lagda.md

@@ -4,6 +4,7 @@ open import Algebra.Prelude
 open import Algebra.Group
 
 open import Cat.Displayed.Univalence.Thin
+open import Cat.Functor.Properties
 open import Cat.Prelude
 ```
 -->

src/Algebra/Group/Cat/Monadic.lagda.md

@@ -9,8 +9,8 @@ open import Algebra.Group
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Adjoint.Monad
 open import Cat.Functor.Equivalence
+open import Cat.Functor.Properties
 open import Cat.Diagram.Monad
-open import Cat.Functor.Base
 
 import Algebra.Group.Cat.Base as Grp
 

src/Algebra/Monoid/Category.lagda.md

@@ -8,8 +8,8 @@ open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Equivalence
 open import Cat.Instances.Delooping
+open import Cat.Functor.Properties
 open import Cat.Functor.Adjoint
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 open import Data.List
@@ -228,8 +228,8 @@ are equivalent to monoid homomorphisms) and that it is [split
 essentially surjective][eso].
 
 [monadic]: Cat.Functor.Adjoint.Monadic.html
-[ff]: Cat.Functor.Base.html#ff-functors
-[eso]: Cat.Functor.Base.html#essential-fibres
+[ff]: Cat.Functor.Properties.html#ff-functors
+[eso]: Cat.Functor.Properties.html#essential-fibres
 
 ```agda
 Monoid-is-monadic : ∀ {ℓ} → is-monadic (Free⊣Forget {ℓ})

src/Cat/Abelian/Instances/Functor.lagda.md

@@ -48,7 +48,7 @@ a group homomorphism.
 
 [$\Ab$-categories]: Cat.Abelian.Base.html#ab-enriched-categories
 [$\Ab$-functors]: Cat.Abelian.Functor.html#ab-enriched-functors
-[functor category]: Cat.Instances.Functor.html
+[functor category]: Cat.Functor.Base.html
 
 ```agda
   Ab-functors : Precategory _ _

src/Cat/Allegory/Base.lagda.md

@@ -28,6 +28,7 @@ disconnected from our theory of bicategories.
 
 ```agda
 record Allegory o ℓ ℓ′ : Type (lsuc (o ⊔ ℓ ⊔ ℓ′)) where
+  no-eta-equality
   field cat : Precategory o ℓ
   open Precategory cat public
 ```

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

@@ -0,0 +1,115 @@
+<!--
+```agda
+open import Cat.Allegory.Base
+open import Cat.Prelude
+
+open import Order.Frame
+
+import Order.Frame.Reasoning
+```
+-->
+
+```agda
+module Cat.Allegory.Instances.Mat where
+```
+
+# Frame-valued matrices
+
+Let $L$ be a [frame]: it could be the frame of opens of a locale, for
+example. It turns out that $L$ has enough structure that we can define
+an [allegory], where the objects are sets, and the morphisms $A \rel B$
+are given by $A \times B$-matrices valued in $L$.
+
+[frame]: Order.Frame.html
+[allegory]: Cat.Allegory.Base.html
+
+<!--
+```agda
+module _ (o : Level) (L : Frame o) where
+  open Order.Frame.Reasoning L hiding (Ob ; Hom-set)
+  open Precategory
+  private module A = Allegory
+```
+-->
+
+The identity matrix has an entry $\top$ at position $(i, j)$ iff $i =
+j$, which we can express independently of whether $i = j$ is decidable
+by saying that the identity matrix has $(i,j)$th entry $\bigvee_{i = j}
+\top$. The composition of $M : B \rel C$ and $N : A \rel B$ has $(a,c)$th
+entry given by
+
+$$
+\bigvee_{b : B} N(a,b) \wedge M(b,c) \text{,}
+$$
+
+which is easily seen to be an analogue of the $\sum_{b = 0}^{B}
+N(a,b)M(b,c)$ which implements composition when matrices take values in
+a ring. The infinite distributive law is applied frequently to establish
+that this is, indeed, a category:
+
+```agda
+  Mat : Precategory (lsuc o) o
+  Mat .Ob          = Set o
+  Mat .Hom A B     = ∣ A ∣ → ∣ B ∣ → ⌞ L ⌟
+  Mat .Hom-set x y = hlevel!
+
+  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)) ⟩
+    ⋃ (λ 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) ⟩
+    ⋃ (λ 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)) ≡⟨ ⋃-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 → 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
+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 .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._◆_ 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._∩_ 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.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 ∩ ⋃ (λ l → h i l ∩ g k l)) ∩ g k j) ≤∎
+```

src/Cat/Allegory/Maps.lagda.md

@@ -3,7 +3,7 @@
 open import Cat.Allegory.Base
 open import Cat.Prelude
 
-import Cat.Allegory.Reasoning as Ar
+import Cat.Allegory.Morphism
 ```
 -->
 
@@ -20,28 +20,32 @@ some category of "sets and relations", to recover the associated
 category of "sets and functions". So, let's start by thinking about $\Rel$!
 
 If you have a relation $R \mono A \times B$, when does it correspond to
-a function $A \to B$? Well, it must definitely be _functional_: if we
+a function $A \to B$? Well, it must definitely be [functional]: if we
 want $R(x, y)$ to represent "$f(x) = y$", then surely if $R(x, y) \land
 R(x, z)$, we must have $y = z$. In allegorical language, we would say
 $RR^o \le \id$, which we can calculate to mean (in $\Rel$) that, for
 all $x, y$,
 
+[functional]: Cat.Allegory.Morphism.html#functional-morphisms
+
 $$
 (\exists z, R(z, x) \land R(z, y)) \to (x = y)\text{.}
 $$
 
-It must also be an _entire_ relation: Every $x$ must at least one $y$ it
+It must also be an [entire] relation: Every $x$ must at least one $y$ it
 is related to, and by functionality, _exactly_ one $y$ it is related to.
 This is the "value of" the function at $y$.
 
+[entire]: Cat.Allegory.Morphism.html#entire-morphisms
+
 ```agda
 module _ {o ℓ h} (A : Allegory o ℓ h) where
-  open Allegory A
+  open Cat.Allegory.Morphism A
   record is-map x y (f : Hom x y) : Type h where
     constructor mapping
     field
-      functional : f ∘ f † ≤ id
-      entire     : id ≤ f † ∘ f
+      functional : is-functional f
+      entire     : is-entire f
 
 module _ {o ℓ h} {A : Allegory o ℓ h} where
   open Allegory A
@@ -87,7 +91,7 @@ arbitrary relations).
 
 ```agda
 module _ {o ℓ h} (A : Allegory o ℓ h) where
-  private module A = Ar A
+  private module A = Cat.Allegory.Morphism A
   open is-map
   open Precategory hiding (_∘_ ; id)
   open A using (_† ; _∘_ ; id ; _◀_ ; _▶_)
@@ -106,21 +110,12 @@ using those words.
 
 ```agda
   Maps[_] .Precategory.id = A.id , mapping
-    (subst (A._≤ id) (sym (A.idl _ ∙ dual-id A)) A.≤-refl)
-    (subst (id A.≤_) (sym (A.idr _ ∙ dual-id A)) A.≤-refl)
-
-  Maps[_] .Precategory._∘_ (f , m) (g , m′) = f A.∘ g , mapping
-    ( (f ∘ g) ∘ (f ∘ g) †     A.=⟨ A.†-inner refl ⟩
-      f ∘ (g ∘ g †) ∘ f †     A.≤⟨ f ▶ m′ .functional ◀ f † ⟩
-      f ∘ id ∘ f †            A.=⟨ A.refl⟩∘⟨ A.idl _ ⟩
-      f ∘ f †                 A.≤⟨ m .functional ⟩
-      id                      A.≤∎ )
-    ( id                   A.≤⟨ m′ .entire ⟩
-      g † ∘ g              A.=⟨ ap (g † ∘_) (sym (A.idl _)) ⟩
-      g † ∘ id ∘ g         A.≤⟨ g † ▶ m .entire ◀ g ⟩
-      g † ∘ (f † ∘ f) ∘ g  A.=⟨ A.pulll (A.pulll (sym A.dual-∘)) ∙ A.pullr refl ⟩
-      (f ∘ g) † ∘ (f ∘ g)  A.≤∎ )
-
+    A.functional-id
+    A.entire-id
+  Maps[_] .Precategory._∘_ (f , m) (g , m′) =
+    f A.∘ g , mapping
+      (A.functional-∘ (m .functional) (m′ .functional))
+      (A.entire-∘ (m .entire) (m′ .entire))
   Maps[_] .idr f = Σ-prop-path (λ _ → hlevel 1) (A.idr _)
   Maps[_] .idl f = Σ-prop-path (λ _ → hlevel 1) (A.idl _)
   Maps[_] .assoc f g h = Σ-prop-path (λ _ → hlevel 1) (A.assoc _ _ _)