defn: Allegory of matrices with values in a frame (#248)

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/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/Order/Frame/Reasoning.lagda.md

@@ -3,6 +3,7 @@
 open import Cat.Prelude
 
 open import Order.Diagram.Lub
+open import Order.Diagram.Glb
 open import Order.Semilattice
 open import Order.Frame
 open import Order.Base
@@ -74,4 +75,52 @@ But this result relies on the cocontinuity of meets.
   ⋃ (λ i → ⋃ F ∩ G i)               ≡⟨ ap ⋃ (funext λ i → ∩-commutative ∙ ⋃-distrib (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 → ⋃ λ 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 _))
+
+⋃-ap
+  : ∀ {I I′ : Type ℓ} {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ⁱ e = ⋃-ap e (λ i → refl)
+⋃-apᶠ p = ⋃-ap (_ , id-equiv) p
+
+⋃-singleton
+  : ∀ {I : Type ℓ} {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)
+
+⋃≤⋃
+  : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟}
+  → (∀ i → f i ≤ g i)
+  → ⋃ f ≤ ⋃ g
+⋃≤⋃ p = ⋃-universal _ (λ i → ≤-trans (p i) (⋃-colimiting _ _))
+
+∩≤∩
+  : ∀ {x y x' y'}
+  → x ≤ x'
+  → y ≤ y'
+  → (x ∩ y) ≤ (x' ∩ y')
+∩≤∩ p q = ∩-univ _ (≤-trans ∩≤l p) (≤-trans ∩≤r q)
 ```