refactor: polish the McBride monad

Author: favonia

src/Mugen/Algebra/Displacement.agda

@@ -50,6 +50,13 @@ record is-displacement
 
   open is-monoid has-is-monoid hiding (has-is-set) public
 
+  abstract
+    right-contract : ∀ {x e} → e ≤ ε → (x ⊗ e) ≤ x
+    right-contract e≤ε = ≤+=→≤ (left-invariant e≤ε) idr
+
+    right-expand : ∀ {x e} → ε ≤ e → x ≤ (x ⊗ e)
+    right-expand ε≤e = =+≤→≤ (sym idr) (left-invariant ε≤e)
+
 record Displacement-on (A : Poset o r) : Type (o ⊔ lsuc r) where
   field
     ε : ⌞ A ⌟

src/Mugen/Cat/HierarchyTheory/McBride.agda

@@ -34,17 +34,22 @@ module _ {A : Poset o r} (𝒟 : Displacement-on A) where
   private
     module ⋉A (L : Poset o (o ⊔ r)) = LeftInvariantRightCentred L A ε
 
+  ⋉A-map-fst : ∀ {L N : Poset o (o ⊔ r)} → Strictly-monotone L N → Strictly-monotone (⋉A.poset L) (⋉A.poset N)
+  ⋉A-map-fst f .hom (l , d) = f .hom l , d
+  ⋉A-map-fst {L} f .pres-≤[]-equal {l1 , d1} {l2 , d2} =
+    let module N⋉A = Reasoning (⋉A.poset _) in
+    ∥-∥-rec (N⋉A.≤[]-is-hlevel 0 $ Poset.Ob-is-set (⋉A.poset L) _ _) λ where
+      (⋉A.biased l1=l2 d1≤d2) →
+        inc (⋉A.biased (ap (f .hom) l1=l2) d1≤d2) , λ p → ap₂ _,_ l1=l2 (ap snd p)
+      (⋉A.centred l1≤l2 d1≤ε ε≤d2) →
+        inc (⋉A.centred (pres-≤ f l1≤l2) d1≤ε ε≤d2) , λ p →
+        ap₂ _,_ (injective-on-related f l1≤l2 (ap fst p)) (ap snd p)
+
   McBride : Hierarchy-theory-on _
   McBride = ht where
     M : Functor (Strict-orders o (o ⊔ r)) (Strict-orders o (o ⊔ r))
     M .F₀ L = ⋉A.poset L
-    M .F₁ f .hom (l , d) = (f .hom l) , d
-    M .F₁ {L} {N} f .pres-≤[]-equal {l1 , d1} {l2 , d2} =
-      let module N⋉A = Reasoning (⋉A.poset N) in
-      ∥-∥-rec (N⋉A.≤[]-is-hlevel 0 $ Poset.Ob-is-set (⋉A.poset L) _ _) λ where
-        (⋉A.biased l1=l2 d1≤d2) → inc (⋉A.biased (ap (f .hom) l1=l2) d1≤d2) , λ p → ap₂ _,_ l1=l2 (ap snd p)
-        (⋉A.centred l1≤l2 d1≤ε ε≤d2) → inc (⋉A.centred (pres-≤ f l1≤l2) d1≤ε ε≤d2) , λ p →
-          ap₂ _,_ (injective-on-related f l1≤l2 (ap fst p)) (ap snd p)
+    M .F₁ = ⋉A-map-fst
     M .F-id = trivial!
     M .F-∘ f g = trivial!
 
@@ -57,35 +62,25 @@ module _ {A : Poset o r} (𝒟 : Displacement-on A) where
     mult .η L .hom ((l , x) , y) = l , (x ⊗ y)
     mult .η L .pres-≤[]-equal {(a1 , d1) , e1} {(a2 , d2) , e2} =
       let module L⋉A = Reasoning (⋉A.poset L) in
-      ∥-∥-rec (L⋉A.≤[]-is-hlevel 0 $ Poset.Ob-is-set (M .F₀ (M .F₀ L)) _ _) lemma where
-        lemma : ⋉A._≤'_ (M .F₀ L) ((a1 , d1) , e1) ((a2 , d2) , e2)
+      ∥-∥-rec (L⋉A.≤[]-is-hlevel 0 $ Poset.Ob-is-set (M .F₀ (M .F₀ L)) _ _) mult-pres where
+        mult-pres : ⋉A._≤'_ (M .F₀ L) ((a1 , d1) , e1) ((a2 , d2) , e2)
           → ⋉A._≤_ L (a1 , (d1 ⊗ e1)) (a2 , (d2 ⊗ e2))
           × ((a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2))
-        lemma (⋉A.biased ad1=ad2 e1≤e2) =
+        mult-pres (⋉A.biased ad1=ad2 e1≤e2) =
           inc (⋉A.biased (ap fst ad1=ad2) (=+≤→≤ (ap (_⊗ e1) (ap snd ad1=ad2)) (left-invariant e1≤e2))) ,
           λ p i → ad1=ad2 i , injectiver-on-related e1≤e2 (ap snd p ∙ ap (_⊗ e2) (sym $ ap snd ad1=ad2)) i
-        lemma (⋉A.centred ad1≤ad2 e1≤ε ε≤e2) = ∥-∥-map lemma₂ ad1≤ad2 , lemma₃ where
-          d1⊗e1≤d1 : (d1 ⊗ e1) ≤ d1
-          d1⊗e1≤d1 = ≤+=→≤ (left-invariant e1≤ε) idr
-
-          d2≤d2⊗e2 : d2 ≤ (d2 ⊗ e2)
-          d2≤d2⊗e2 = =+≤→≤ (sym idr) (left-invariant ε≤e2)
-
-          lemma₂ : ⋉A._≤'_ L (a1 , d1) (a2 , d2)
-            → ⋉A._≤'_ L (a1 , (d1 ⊗ e1)) (a2 , (d2 ⊗ e2))
-          lemma₂ (⋉A.biased a1=a2 d1≤d2) = ⋉A.biased a1=a2 (≤-trans d1⊗e1≤d1 (≤-trans d1≤d2 d2≤d2⊗e2))
-          lemma₂ (⋉A.centred a1≤a2 d1≤ε ε≤d2) = ⋉A.centred a1≤a2 (≤-trans d1⊗e1≤d1 d1≤ε) (≤-trans ε≤d2 d2≤d2⊗e2)
-
-          lemma₃ : (a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2)
-          lemma₃ p i = (a1=a2 i , d1=d2 i) , e1=e2 i where
-            a1=a2 : a1 ≡ a2
-            a1=a2 = ap fst p
+        mult-pres (⋉A.centred ad1≤ad2 e1≤ε ε≤e2) = ∥-∥-map push-⊗ ad1≤ad2 , mult-inj where
+          push-⊗ : ⋉A._≤'_ L (a1 , d1) (a2 , d2) → ⋉A._≤'_ L (a1 , (d1 ⊗ e1)) (a2 , (d2 ⊗ e2))
+          push-⊗ (⋉A.biased a1=a2 d1≤d2) = ⋉A.biased a1=a2 (≤-trans (right-contract e1≤ε) (≤-trans d1≤d2 (right-expand ε≤e2)))
+          push-⊗ (⋉A.centred a1≤a2 d1≤ε ε≤d2) = ⋉A.centred a1≤a2 (≤-trans (right-contract e1≤ε) d1≤ε) (≤-trans ε≤d2 (right-expand ε≤e2))
 
+          mult-inj : (a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2)
+          mult-inj p i = (fst (p i) , d1=d2 i) , e1=e2 i where
             d2≤d1 : d2 ≤ d1
             d2≤d1 = begin-≤
-              d2      ≤⟨ d2≤d2⊗e2 ⟩
+              d2      ≤⟨ right-expand ε≤e2 ⟩
               d2 ⊗ e2 ≐⟨ sym $ ap snd p ⟩
-              d1 ⊗ e1 ≤⟨ d1⊗e1≤d1 ⟩
+              d1 ⊗ e1 ≤⟨ right-contract e1≤ε ⟩
               d1      ≤∎
 
             d1=d2 : d1 ≡ d2