WIP

src/Mugen/Cat/HierarchyTheory/McBrideFunctoriality.agda

@@ -0,0 +1,43 @@
+module Mugen.Cat.HierarchyTheory.McBrideFunctoriality 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.HierarchyTheories
+open import Mugen.Cat.Instances.Displacements
+
+open import Mugen.Cat.HierarchyTheory
+open import Mugen.Cat.HierarchyTheory.McBride
+
+import Mugen.Order.Reasoning
+
+private variable
+  o o' r r' : Level
+
+--------------------------------------------------------------------------------
+-- The Additional Functoriality of McBride Hierarchy Theory
+--
+-- The McBride monad is functorial in the parameter displacement.
+
+module _ where
+  open Strictly-monotone
+  open Functor
+  open _=>_
+  open Monad-hom
+
+  McBride-functor : Functor (Displacements o r) (Hierarchy-theories o (o ⊔ r))
+  McBride-functor .F₀ (_ , 𝒟) = McBride 𝒟
+  McBride-functor .F₁ σ .nat .η L .hom (α , d) = α , (σ # d)
+  McBride-functor .F₁ {A , 𝒟} {B , ℰ} σ .nat .η L .pres-≤[]-equal {α1 , d1} {α2 , d2} p =
+    let module 𝒟 = Displacement-on 𝒟
+        module L⋉A = Mugen.Order.Reasoning (L ⋉[ 𝒟.ε ] A)
+        module L⋉B = Mugen.Order.Reasoning (L ⋉[ 𝒟.ε ] B)
+    in
+    ∥-∥-rec (L⋉B.≤[]-is-hlevel 0 $ Poset.Ob-is-set (L ⋉[ 𝒟.ε ] B) _ _) ? p