feat: McBride monad is functorial in its displacement algebra

Dockerfile

@@ -31,7 +31,7 @@ FROM alpine AS onelab
 RUN apk add --no-cache git
 
 WORKDIR /dist/1lab
-ARG ONELAB_VERSION=c27000e087bd1233647a20ba02777cd3b4aa2b38
+ARG ONELAB_VERSION=5cb0edee762e05f14869817fbed5af3412da5e1f
 RUN \
   git init && \
   git remote add origin https://github.com/plt-amy/1lab && \

src/Mugen/Algebra/Displacement/Action.agda

@@ -53,7 +53,8 @@ module _ where
 instance
   Right-actionlike-displacement-action
     : ∀ {o r o' r'}
-    → Right-actionlike (λ A (B : Σ _ Displacement-on) → Right-displacement-action {o} {r} {o'} {r'} A (B .snd))
+    → Right-actionlike λ (A : Poset o r) (B : Σ (Poset o' r') Displacement-on) →
+      Right-displacement-action A (B .snd)
   Right-actionlike.⟦ Right-actionlike-displacement-action ⟧ʳ =
     Right-displacement-action._⋆_
   Right-actionlike-displacement-action .Right-actionlike.extʳ =

src/Mugen/Cat/HierarchyTheory.agda

@@ -1,21 +1,27 @@
 module Mugen.Cat.HierarchyTheory where
 
-open import Cat.Diagram.Monad
 import Cat.Reasoning as Cat
+open import Cat.Diagram.Monad
+open import Cat.Instances.Monads
 
 open import Mugen.Prelude
 open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Order.StrictOrder
 
 --------------------------------------------------------------------------------
--- Heirarchy Theories
+-- Hierarchy Theories
 --
--- A heirarchy theory is defined to be a monad on the category of strict orders.
--- We also define the McBride Heirarchy Theory.
+-- A hierarchy theory is defined to be a monad on the category of strict orders.
+-- We also define the McBride Hierarchy Theory.
 
 Hierarchy-theory : ∀ o r → Type (lsuc o ⊔ lsuc r)
 Hierarchy-theory o r = Monad (Strict-orders o r)
 
+-- And they form a category
+
+Hierarchy-theories : ∀ o r → Precategory (lsuc (o ⊔ r)) (lsuc (o ⊔ r))
+Hierarchy-theories o r = Monads (Strict-orders o r)
+
 --------------------------------------------------------------------------------
 -- Misc. Definitions
 

src/Mugen/Cat/HierarchyTheory/McBride.agda

@@ -1,15 +1,18 @@
 module Mugen.Cat.HierarchyTheory.McBride where
 
 open import Cat.Diagram.Monad
+open import Cat.Instances.Monads
+open import Cat.Displayed.Total
 
 open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 open import Mugen.Order.Instances.LeftInvariantRightCentered
 open import Mugen.Order.StrictOrder
 open import Mugen.Cat.Instances.StrictOrders
+open import Mugen.Cat.Instances.Displacements
 open import Mugen.Cat.HierarchyTheory
 
-import Mugen.Order.Reasoning
+import Mugen.Order.Reasoning as Reasoning
 
 private variable
   o o' r r' : Level
@@ -21,20 +24,21 @@ private variable
 -- A construction of the McBride Monad for any displacement algebra '𝒟'
 
 module _ {A : Poset o r} (𝒟 : Displacement-on A) where
-  open Displacement-on 𝒟
-  open Mugen.Order.Reasoning A
-
-  open Strictly-monotone
   open Functor
   open _=>_
+  open Strictly-monotone
+
+  open Reasoning A
+  open Displacement-on 𝒟
 
   McBride : Hierarchy-theory o (o ⊔ r)
   McBride = ht where
     M : Functor (Strict-orders o (o ⊔ r)) (Strict-orders o (o ⊔ r))
     M .F₀ L = L ⋉[ ε ] A
     M .F₁ f .hom (l , d) = (f .hom l) , d
     M .F₁ {L} {N} f .pres-≤[]-equal {l1 , d1} {l2 , d2} =
-      ∥-∥-rec (×-is-hlevel 1 squash $ Π-is-hlevel 1 λ _ → Poset.Ob-is-set (M .F₀ L) _ _) λ where
+      let module N⋉A = Reasoning (N ⋉[ ε ] A) in
+      ∥-∥-rec (N⋉A.≤[]-is-hlevel 0 $ Poset.Ob-is-set (L ⋉[ ε ] A) _ _) λ where
         (biased l1=l2 d1≤d2) → inc (biased (ap (f .hom) l1=l2) d1≤d2) , λ p → ap₂ _,_ l1=l2 (ap snd p)
         (centred l1≤l2 d1≤ε ε≤d2) → inc (centred (pres-≤ f l1≤l2) d1≤ε ε≤d2) , λ p →
           ap₂ _,_ (injective-on-related f l1≤l2 (ap fst p)) (ap snd p)
@@ -49,7 +53,8 @@ module _ {A : Poset o r} (𝒟 : Displacement-on A) where
     mult : M F∘ M => M
     mult .η L .hom ((l , x) , y) = l , (x ⊗ y)
     mult .η L .pres-≤[]-equal {(a1 , d1) , e1} {(a2 , d2) , e2} =
-      ∥-∥-rec (×-is-hlevel 1 squash $ Π-is-hlevel 1 λ _ → Poset.Ob-is-set (M .F₀ (M .F₀ L)) _ _) lemma where
+      let module L⋉A = Reasoning (L ⋉[ ε ] A) in
+      ∥-∥-rec (L⋉A.≤[]-is-hlevel 0 $ Poset.Ob-is-set (M .F₀ (M .F₀ L)) _ _) lemma where
         lemma : (M .F₀ L) ⋉[ ε ] A [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ]
           → (L ⋉[ ε ] A [ (a1 , (d1 ⊗ e1)) ≤ (a2 , (d2 ⊗ e2)) ])
           × ((a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2))
@@ -94,3 +99,42 @@ module _ {A : Poset o r} (𝒟 : Displacement-on A) where
     ht .Monad.left-ident = ext λ α d → (refl , idl {d})
     ht .Monad.right-ident = ext λ α d → (refl , idr {d})
     ht .Monad.mult-assoc = ext λ α d1 d2 d3 → (refl , sym (associative {d1} {d2} {d3}))
+
+--------------------------------------------------------------------------------
+-- The Additional Functoriality of McBride Hierarchy Theory
+--
+-- The McBride monad is functorial in the parameter displacement.
+
+module _ where
+  open Functor
+  open _=>_
+  open Monad-hom
+  open Total-hom
+  open Strictly-monotone
+  open Displacement-on
+  open is-displacement-hom
+
+  McBride-functor : Functor (Displacements o r) (Hierarchy-theories o (o ⊔ r))
+  McBride-functor .F₀ (_ , 𝒟) = McBride 𝒟
+  McBride-functor .F₁ σ .nat .η L .hom (l , d) = l , σ .hom # d
+  McBride-functor .F₁ {A , 𝒟} {B , ℰ} σ .nat .η L .pres-≤[]-equal {l1 , d1} {l2 , d2} =
+    let module A = Reasoning A
+        module B = Reasoning B
+        module σ = Strictly-monotone (σ .hom)
+        module L⋉A = Reasoning (L ⋉[ 𝒟 .ε ] A)
+        module L⋉B = Reasoning (L ⋉[ ℰ .ε ] B)
+    in
+    ∥-∥-rec (L⋉B.≤[]-is-hlevel 0 $ L⋉A.Ob-is-set _ _) λ where
+      (biased l1=l2 d1≤d2) →
+        inc (biased l1=l2 (σ.pres-≤ d1≤d2)) ,
+        λ p → ap₂ _,_ (ap fst p) (σ.injective-on-related d1≤d2 $ ap snd p)
+      (centred l1≤l2 d1≤ε ε≤d2) →
+        inc (centred l1≤l2
+          (B.≤+=→≤ (σ.pres-≤ d1≤ε) (σ .preserves .pres-ε))
+          (B.=+≤→≤ (sym $ σ .preserves .pres-ε) (σ.pres-≤ ε≤d2))) ,
+        λ p → ap₂ _,_ (ap fst p) (σ.injective-on-related (A.≤-trans d1≤ε ε≤d2) $ ap snd p)
+  McBride-functor .F₁ σ .nat .is-natural L N f = trivial!
+  McBride-functor .F₁ σ .pres-unit = ext λ L l → refl , σ .preserves .pres-ε
+  McBride-functor .F₁ σ .pres-mult = ext λ L l d1 d2 → refl , σ .preserves .pres-⊗
+  McBride-functor .F-id = trivial!
+  McBride-functor .F-∘ f g = trivial!

src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda

@@ -188,7 +188,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
   T : Functor (Endos SOrdᴴ (Fᴴ₀ Δ)) (Endos SOrdᴹᴰ (Fᴹᴰ₀ (Disc Ψ)))
   T .Functor.F₀ _ = tt
   T .Functor.F₁ σ .morphism .hom (α , d) = α , (T′ σ SOrdᴴ.∘ d)
-  T .Functor.F₁ σ .morphism .pres-≤[]-equal {α , d1} {β , d2} p =
+  T .Functor.F₁ σ .morphism .pres-≤[]-equal {α1 , d1} {α2 , d2} p =
     let d1≤d2 , injr = 𝒟.left-strict-invariant {T′ σ} {d1} {d2} (⋉-snd-invariant p) in
     inc (biased (⋉-fst-invariant p) d1≤d2) , λ q i → q i .fst , injr (ap snd q) i
   T .Functor.F₁ σ .commutes = trivial!

src/Mugen/Cat/README.md

@@ -1,4 +1,4 @@
 # Categorical Properties
 
-This directory formalizes various categorical results, focusing on the definition of [heirarchy theories](HierarchyTheory.agda),
-as well as the first steps towards proving that the [McBride Heirarchy Theory is universal](HierarchyTheory/).
+This directory formalizes various categorical results, focusing on the definition of [hierarchy theories](HierarchyTheory.agda),
+as well as the first steps towards proving that the [McBride Hierarchy Theory is universal](HierarchyTheory/Universality/).

src/Mugen/Order/StrictOrder.agda

@@ -19,8 +19,11 @@ record Strictly-monotone (X : Poset o r) (Y : Poset o' r') : Type (o ⊔ o' ⊔
 
     -- Preserving parametrized inequalities
     --
-    -- This is morally '∀ {x y} → x X.≤[ x ≡ y ] y → hom x Y.≤[ x ≡ y ] hom y'
-    -- and is equivalent to pres-≤[] below.
+    -- This is constructively equivalent to
+    -- 1. ∀ {x y} → x X.≤[ x ≡ y ] y → hom x Y.≤[ x ≡ y ] hom y
+    -- 2. ∀ {K} {x y} → x X.≤[ K ] y → hom x Y.≤[ K ] hom y
+    -- and classically equivalent to
+    -- 1. ∀ {x y} → x X.≤[ ⊥ ] y → hom x Y.≤[ ⊥ ] hom y
     pres-≤[]-equal : ∀ {x y} → x X.≤ y → hom x Y.≤[ x ≡ y ] hom y
 
   abstract
@@ -61,7 +64,7 @@ instance
     : ∀ {ℓ} {X : Poset o r} {Y : Poset o' r'}
     → ⦃ sa : Extensional (⌞ X ⌟ → ⌞ Y ⌟) ℓ ⦄
     → Extensional (Strictly-monotone X Y) ℓ
-  Extensional-Strictly-monotone {Y = Y} ⦃ sa ⦄ =
+  Extensional-Strictly-monotone ⦃ sa ⦄ =
     injection→extensional!
       {f = Strictly-monotone.hom}
       (Strictly-monotone-path _ _) sa