From 459d63db5ad1a0561ed5fa1c545057b9fb6d08dc Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 26 Nov 2023 22:31:52 -0600 Subject: [PATCH] refactor: split Cat.HierarchyTheory into multiple files --- .../Algebra/Displacement/Endomorphism.agda | 6 +- src/Mugen/Cat/HierarchyTheory.agda | 127 ------------------ src/Mugen/Cat/HierarchyTheory/Properties.agda | 6 +- src/Mugen/Cat/McBrideMonad.agda | 103 ++++++++++++++ src/Mugen/Cat/Monad.agda | 41 ++++++ src/Mugen/Everything.agda | 2 + 6 files changed, 153 insertions(+), 132 deletions(-) create mode 100644 src/Mugen/Cat/McBrideMonad.agda create mode 100644 src/Mugen/Cat/Monad.agda diff --git a/src/Mugen/Algebra/Displacement/Endomorphism.agda b/src/Mugen/Algebra/Displacement/Endomorphism.agda index 5aba40d..85b9283 100644 --- a/src/Mugen/Algebra/Displacement/Endomorphism.agda +++ b/src/Mugen/Algebra/Displacement/Endomorphism.agda @@ -13,7 +13,7 @@ open import Mugen.Data.NonEmpty open import Mugen.Algebra.Displacement open import Mugen.Order.Poset open import Mugen.Cat.StrictOrders -open import Mugen.Cat.HierarchyTheory +open import Mugen.Cat.Monad -------------------------------------------------------------------------------- -- Endomorphism Displacements @@ -89,7 +89,7 @@ module _ {o r} (H : Monad (Strict-orders o r)) (Δ : Poset o r) where endo≤-trans σ δ τ (lift σ≤δ) (lift δ≤τ) = lift λ α → H⟨Δ⟩.≤-trans (σ≤δ α) (δ≤τ α) endo≤-antisym : ∀ σ δ → endo[ σ ≤ δ ] → endo[ δ ≤ σ ] → σ ≡ δ - endo≤-antisym σ δ (lift σ≤δ) (lift δ≤σ) = free-algebra-hom-path $ ext λ α → + endo≤-antisym σ δ (lift σ≤δ) (lift δ≤σ) = free-algebra-hom-path H $ ext λ α → H⟨Δ⟩.≤-antisym (σ≤δ α) (δ≤σ α) -------------------------------------------------------------------------------- @@ -99,7 +99,7 @@ module _ {o r} (H : Monad (Strict-orders o r)) (Δ : Poset o r) where ∘-left-invariant σ δ τ δ≤τ = lift λ α → σ .morphism .Strictly-monotone.mono (δ≤τ .Lift.lower α) ∘-injr-on-≤ : ∀ (σ δ τ : Endomorphism) → endo[ δ ≤ τ ] → σ ∘ δ ≡ σ ∘ τ → δ ≡ τ - ∘-injr-on-≤ σ δ τ (lift δ≤τ) p = free-algebra-hom-path $ ext λ α → + ∘-injr-on-≤ σ δ τ (lift δ≤τ) p = free-algebra-hom-path H $ ext λ α → σ .morphism .Strictly-monotone.inj-on-related (δ≤τ α) (ap (_# (unit.η Δ # α)) p) -------------------------------------------------------------------------------- diff --git a/src/Mugen/Cat/HierarchyTheory.agda b/src/Mugen/Cat/HierarchyTheory.agda index 2735406..55222e6 100644 --- a/src/Mugen/Cat/HierarchyTheory.agda +++ b/src/Mugen/Cat/HierarchyTheory.agda @@ -4,17 +4,9 @@ open import Cat.Diagram.Monad import Cat.Reasoning as Cat open import Mugen.Prelude -open import Mugen.Algebra.Displacement open import Mugen.Cat.StrictOrders -open import Mugen.Order.LeftInvariantRightCentered open import Mugen.Order.Poset -import Mugen.Order.Reasoning - -open Strictly-monotone -open Functor -open _=>_ - -------------------------------------------------------------------------------- -- Heirarchy Theories -- @@ -24,125 +16,6 @@ open _=>_ Hierarchy-theory : ∀ o r → Type (lsuc o ⊔ lsuc r) Hierarchy-theory o r = Monad (Strict-orders o r) --------------------------------------------------------------------------------- --- The McBride Hierarchy Theory --- Section 3.1 --- --- A construction of the McBride Monad for any displacement algebra '𝒟' - -ℳ : ∀ {o} → Displacement-algebra o o → Hierarchy-theory o o -ℳ {o = o} 𝒟 = ht where - open Displacement-algebra 𝒟 - open Mugen.Order.Reasoning poset - - M : Functor (Strict-orders o o) (Strict-orders o o) - M .F₀ L = L ⋉[ ε ] poset - M .F₁ f .hom (l , d) = (f .hom l) , d - M .F₁ {L} {N} f .mono {l1 , d1} {l2 , d2} = ∥-∥-map λ where - (biased l1=l2 d1≤d2) → biased (ap (f .hom) l1=l2) d1≤d2 - (centred l1≤l2 d1≤ε ε≤d2) → centred (f .mono l1≤l2) d1≤ε ε≤d2 - M .F₁ {L} {N} f .inj-on-related {l1 , d1} {l2 , d2} = - ∥-∥-rec (Π-is-hlevel 1 λ _ → Poset.has-is-set (M .F₀ L) _ _) λ where - (biased l1=l2 _) p → ap₂ _,_ l1=l2 (ap snd p) - (centred l1≤l2 _ _) p → ap₂ _,_ (f .inj-on-related l1≤l2 (ap fst p)) (ap snd p) - M .F-id = trivial! - M .F-∘ f g = trivial! - - unit : Id => M - unit .η L .hom l = l , ε - unit .η L .mono l1≤l2 = inc (centred l1≤l2 ≤-refl ≤-refl) - unit .η L .inj-on-related _ p = ap fst p - unit .is-natural L L' f = trivial! - - mult : M F∘ M => M - mult .η L .hom ((l , x) , y) = l , (x ⊗ y) - mult .η L .mono {(a1 , d1) , e1} {(a2 , d2) , e2} = - ∥-∥-rec squash lemma where - lemma : (M .F₀ L) ⋉[ ε ] poset [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ] - → L ⋉[ ε ] poset [ (a1 , (d1 ⊗ e1)) ≤ (a2 , (d2 ⊗ e2)) ] - lemma (biased ad1=ad2 e1≤e2) = - inc (biased (ap fst ad1=ad2) (=+≤→≤ (ap (_⊗ e1) (ap snd ad1=ad2)) (≤-left-invariant e1≤e2))) - lemma (centred ad1≤ad2 e1≤ε ε≤e2) = ∥-∥-map lemma₂ ad1≤ad2 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₂ : L ⋉[ ε ] poset [ (a1 , d1) raw≤ (a2 , d2) ] - → L ⋉[ ε ] poset [ (a1 , (d1 ⊗ e1)) raw≤ (a2 , (d2 ⊗ e2)) ] - lemma₂ (biased a1=a2 d1≤d2) = biased a1=a2 (≤-trans d1⊗e1≤d1 (≤-trans d1≤d2 d2≤d2⊗e2)) - lemma₂ (centred a1≤a2 d1≤ε ε≤d2) = centred a1≤a2 (≤-trans d1⊗e1≤d1 d1≤ε) (≤-trans ε≤d2 d2≤d2⊗e2) - mult .η L .inj-on-related {(a1 , d1) , e1} {(a2 , d2) , e2} = - ∥-∥-rec (Π-is-hlevel 1 λ _ → Poset.has-is-set (M .F₀ (M .F₀ L)) _ _) lemma where - lemma : (M .F₀ L) ⋉[ ε ] poset [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ] - → (a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) - → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2) - lemma (biased ad1=ad2 e1≤e2) p i = - ad1=ad2 i , injr-on-≤ e1≤e2 (ap snd p ∙ ap (_⊗ e2) (sym $ ap snd ad1=ad2)) i - lemma (centred ad1≤ad2 e1≤ε ε≤e2) p i = (a1=a2 i , d1=d2 i) , e1=e2 i where - a1=a2 : a1 ≡ a2 - a1=a2 = ap fst p - - d2≤d1 : d2 ≤ d1 - d2≤d1 = - d2 ≐⟨ sym idr ⟩ - d2 ⊗ ε ≤⟨ ≤-left-invariant ε≤e2 ⟩ - d2 ⊗ e2 ≐⟨ sym $ ap snd p ⟩ - d1 ⊗ e1 ≤⟨ ≤-left-invariant e1≤ε ⟩ - d1 ⊗ ε ≐⟨ idr ⟩ - d1 ≤∎ - - d1=d2 : d1 ≡ d2 - d1=d2 = ≤-antisym (⋉-snd-invariant ad1≤ad2) d2≤d1 - - e1=e2 : e1 ≡ e2 - e1=e2 = injr-on-≤ (≤-trans e1≤ε ε≤e2) $ ap snd p ∙ ap (_⊗ e2) (sym d1=d2) - mult .is-natural L L' f = trivial! - - ht : Hierarchy-theory o o - ht .Monad.M = M - ht .Monad.unit = unit - ht .Monad.mult = mult - ht .Monad.left-ident = ext λ where - (α , d) → (refl , idl {d}) - ht .Monad.right-ident = ext λ where - (α , d) → (refl , idr {d}) - ht .Monad.mult-assoc = ext λ where - (((α , d1) , d2) , d3) → (refl , sym (associative {d1} {d2} {d3})) - --------------------------------------------------------------------------------- --- Hierarchy Theory Algebras - -module _ {o r} {H : Hierarchy-theory o r} where - private - module H = Monad H - - Free⟨_⟩ : Poset o r → Algebra (Strict-orders o r) H - Free⟨_⟩ = Functor.F₀ (Free (Strict-orders o r) H) - - open Cat (Strict-orders o r) - open Algebra-hom - - -- NOTE: We can't use any fancy reasoning combinators in this proof, as it really - -- upsets the unifier, as it will fail to unify the homomorphism proofs... - free-algebra-hom-path : ∀ {X Y} {f g : Algebra-hom (Strict-orders o r) H Free⟨ X ⟩ Free⟨ Y ⟩} - → f .morphism ∘ H.unit.η _ ≡ (g .morphism ∘ H.unit.η _) - → f ≡ g - free-algebra-hom-path {f = f} {g = g} p = Algebra-hom-path _ $ - f .morphism ≡⟨ intror H.left-ident ⟩ - f .morphism ∘ H.mult.η _ ∘ H.M₁ (H.unit.η _) ≡⟨ assoc (f .morphism) (H.mult.η _) (H.M₁ (H.unit.η _)) ⟩ - (f .morphism ∘ H.mult.η _) ∘ H.M₁ (H.unit.η _) ≡⟨ ap (_∘ H.M₁ (H.unit.η _)) (f .commutes) ⟩ - (H.mult.η _ ∘ H.M₁ (f .morphism)) ∘ H.M₁ (H.unit.η _) ≡˘⟨ assoc (H.mult.η _) (H.M₁ (f .morphism)) (H.M₁ (H.unit.η _)) ⟩ - H.mult.η _ ∘ H.M₁ (f .morphism) ∘ H.M₁ (H.unit.η _) ≡˘⟨ ap (H.mult.η _ ∘_) (H.M-∘ _ _) ⟩ - H.mult.η _ ∘ H.M₁ (f .morphism ∘ H.unit.η _) ≡⟨ ap (λ ϕ → H.mult.η _ ∘ H.M₁ ϕ) p ⟩ - H.mult.η _ ∘ H.M₁ (g .morphism ∘ H.unit.η _) ≡⟨ ap (H.mult.η _ ∘_) (H.M-∘ _ _) ⟩ - H.mult.η _ ∘ H.M₁ (g .morphism) ∘ H.M₁ (H.unit.η _) ≡⟨ assoc (H.mult.η _) (H.M₁ (g .morphism)) (H.M₁ (H.unit.η _)) ⟩ - (H.mult.η _ ∘ H.M₁ (g .morphism)) ∘ H.M₁ (H.unit.η _) ≡˘⟨ ap (_∘ H.M₁ (H.unit.η _)) (g .commutes) ⟩ - (g .morphism ∘ H.mult.η _) ∘ H.M₁ (H.unit.η _) ≡˘⟨ assoc (g .morphism) (H.mult.η _) (H.M₁ (H.unit.η _)) ⟩ - g .morphism ∘ H.mult.η _ ∘ H.M₁ (H.unit.η _) ≡⟨ elimr H.left-ident ⟩ - g .morphism ∎ - -------------------------------------------------------------------------------- -- Misc. Definitions diff --git a/src/Mugen/Cat/HierarchyTheory/Properties.agda b/src/Mugen/Cat/HierarchyTheory/Properties.agda index 9c0d258..8504e2d 100644 --- a/src/Mugen/Cat/HierarchyTheory/Properties.agda +++ b/src/Mugen/Cat/HierarchyTheory/Properties.agda @@ -14,8 +14,10 @@ open import Mugen.Algebra.Displacement open import Mugen.Algebra.Displacement.Endomorphism open import Mugen.Cat.Endomorphisms -open import Mugen.Cat.HierarchyTheory open import Mugen.Cat.StrictOrders +open import Mugen.Cat.Monad +open import Mugen.Cat.HierarchyTheory +open import Mugen.Cat.McBrideMonad open import Mugen.Order.Coproduct open import Mugen.Order.LeftInvariantRightCentered @@ -287,7 +289,7 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T T-faithful pt H-preserves-monos {x} {y} {σ} {δ} p = - free-algebra-hom-path $ H-preserves-monos ι₁-hom ι₁-monic _ _ $ + free-algebra-hom-path H $ H-preserves-monos ι₁-hom ι₁-monic _ _ $ ext λ α → σ̅ σ # (ι₁ α) ≡˘⟨ H.right-ident #ₚ _ ⟩ H.mult.η _ # (H.unit.η _ # (σ̅ σ # (ι₁ α))) ≡⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (σ̅ σ) #ₚ _) ⟩ diff --git a/src/Mugen/Cat/McBrideMonad.agda b/src/Mugen/Cat/McBrideMonad.agda new file mode 100644 index 0000000..2d6e758 --- /dev/null +++ b/src/Mugen/Cat/McBrideMonad.agda @@ -0,0 +1,103 @@ +module Mugen.Cat.McBrideMonad where + +open import Cat.Diagram.Monad + +open import Mugen.Prelude +open import Mugen.Algebra.Displacement +open import Mugen.Order.LeftInvariantRightCentered +open import Mugen.Order.Poset +open import Mugen.Cat.StrictOrders +open import Mugen.Cat.HierarchyTheory + +import Mugen.Order.Reasoning + +-------------------------------------------------------------------------------- +-- The McBride Hierarchy Theory +-- Section 3.1 +-- +-- A construction of the McBride Monad for any displacement algebra '𝒟' + +ℳ : ∀ {o} → Displacement-algebra o o → Hierarchy-theory o o +ℳ {o = o} 𝒟 = ht where + open Displacement-algebra 𝒟 + open Mugen.Order.Reasoning poset + + open Strictly-monotone + open Functor + open _=>_ + + M : Functor (Strict-orders o o) (Strict-orders o o) + M .F₀ L = L ⋉[ ε ] poset + M .F₁ f .hom (l , d) = (f .hom l) , d + M .F₁ {L} {N} f .mono {l1 , d1} {l2 , d2} = ∥-∥-map λ where + (biased l1=l2 d1≤d2) → biased (ap (f .hom) l1=l2) d1≤d2 + (centred l1≤l2 d1≤ε ε≤d2) → centred (f .mono l1≤l2) d1≤ε ε≤d2 + M .F₁ {L} {N} f .inj-on-related {l1 , d1} {l2 , d2} = + ∥-∥-rec (Π-is-hlevel 1 λ _ → Poset.has-is-set (M .F₀ L) _ _) λ where + (biased l1=l2 _) p → ap₂ _,_ l1=l2 (ap snd p) + (centred l1≤l2 _ _) p → ap₂ _,_ (f .inj-on-related l1≤l2 (ap fst p)) (ap snd p) + M .F-id = trivial! + M .F-∘ f g = trivial! + + unit : Id => M + unit .η L .hom l = l , ε + unit .η L .mono l1≤l2 = inc (centred l1≤l2 ≤-refl ≤-refl) + unit .η L .inj-on-related _ p = ap fst p + unit .is-natural L L' f = trivial! + + mult : M F∘ M => M + mult .η L .hom ((l , x) , y) = l , (x ⊗ y) + mult .η L .mono {(a1 , d1) , e1} {(a2 , d2) , e2} = + ∥-∥-rec squash lemma where + lemma : (M .F₀ L) ⋉[ ε ] poset [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ] + → L ⋉[ ε ] poset [ (a1 , (d1 ⊗ e1)) ≤ (a2 , (d2 ⊗ e2)) ] + lemma (biased ad1=ad2 e1≤e2) = + inc (biased (ap fst ad1=ad2) (=+≤→≤ (ap (_⊗ e1) (ap snd ad1=ad2)) (≤-left-invariant e1≤e2))) + lemma (centred ad1≤ad2 e1≤ε ε≤e2) = ∥-∥-map lemma₂ ad1≤ad2 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₂ : L ⋉[ ε ] poset [ (a1 , d1) raw≤ (a2 , d2) ] + → L ⋉[ ε ] poset [ (a1 , (d1 ⊗ e1)) raw≤ (a2 , (d2 ⊗ e2)) ] + lemma₂ (biased a1=a2 d1≤d2) = biased a1=a2 (≤-trans d1⊗e1≤d1 (≤-trans d1≤d2 d2≤d2⊗e2)) + lemma₂ (centred a1≤a2 d1≤ε ε≤d2) = centred a1≤a2 (≤-trans d1⊗e1≤d1 d1≤ε) (≤-trans ε≤d2 d2≤d2⊗e2) + mult .η L .inj-on-related {(a1 , d1) , e1} {(a2 , d2) , e2} = + ∥-∥-rec (Π-is-hlevel 1 λ _ → Poset.has-is-set (M .F₀ (M .F₀ L)) _ _) lemma where + lemma : (M .F₀ L) ⋉[ ε ] poset [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ] + → (a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) + → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2) + lemma (biased ad1=ad2 e1≤e2) p i = + ad1=ad2 i , injr-on-≤ e1≤e2 (ap snd p ∙ ap (_⊗ e2) (sym $ ap snd ad1=ad2)) i + lemma (centred ad1≤ad2 e1≤ε ε≤e2) p i = (a1=a2 i , d1=d2 i) , e1=e2 i where + a1=a2 : a1 ≡ a2 + a1=a2 = ap fst p + + d2≤d1 : d2 ≤ d1 + d2≤d1 = + d2 ≐⟨ sym idr ⟩ + d2 ⊗ ε ≤⟨ ≤-left-invariant ε≤e2 ⟩ + d2 ⊗ e2 ≐⟨ sym $ ap snd p ⟩ + d1 ⊗ e1 ≤⟨ ≤-left-invariant e1≤ε ⟩ + d1 ⊗ ε ≐⟨ idr ⟩ + d1 ≤∎ + + d1=d2 : d1 ≡ d2 + d1=d2 = ≤-antisym (⋉-snd-invariant ad1≤ad2) d2≤d1 + + e1=e2 : e1 ≡ e2 + e1=e2 = injr-on-≤ (≤-trans e1≤ε ε≤e2) $ ap snd p ∙ ap (_⊗ e2) (sym d1=d2) + mult .is-natural L L' f = trivial! + + ht : Hierarchy-theory o o + ht .Monad.M = M + ht .Monad.unit = unit + ht .Monad.mult = mult + ht .Monad.left-ident = ext λ where + (α , d) → (refl , idl {d}) + ht .Monad.right-ident = ext λ where + (α , d) → (refl , idr {d}) + ht .Monad.mult-assoc = ext λ where + (((α , d1) , d2) , d3) → (refl , sym (associative {d1} {d2} {d3})) diff --git a/src/Mugen/Cat/Monad.agda b/src/Mugen/Cat/Monad.agda new file mode 100644 index 0000000..3507515 --- /dev/null +++ b/src/Mugen/Cat/Monad.agda @@ -0,0 +1,41 @@ +module Mugen.Cat.Monad where + +open import Cat.Diagram.Monad +import Cat.Reasoning as Cat + +open import Mugen.Prelude +open import Mugen.Order.Poset + +-------------------------------------------------------------------------------- +-- Misc. Lemmas for Monads + +module _ {o r} {C : Precategory o r} (M : Monad C) where + private + module M = Monad M + + open Cat C + open Algebra-hom + + Free⟨_⟩ : C .Precategory.Ob → Algebra C M + Free⟨_⟩ = Functor.F₀ (Free C M) + + -- Favonia: does this lemma belong to 1lab? + -- + -- NOTE: We can't use any fancy reasoning combinators in this proof, as it really + -- upsets the unifier, as it will fail to unify the homomorphism proofs... + free-algebra-hom-path : ∀ {X Y} {f g : Algebra-hom C M Free⟨ X ⟩ Free⟨ Y ⟩} + → f .morphism ∘ M.unit.η _ ≡ (g .morphism ∘ M.unit.η _) + → f ≡ g + free-algebra-hom-path {f = f} {g = g} p = Algebra-hom-path _ $ + f .morphism ≡⟨ intror M.left-ident ⟩ + f .morphism ∘ M.mult.η _ ∘ M.M₁ (M.unit.η _) ≡⟨ assoc (f .morphism) (M.mult.η _) (M.M₁ (M.unit.η _)) ⟩ + (f .morphism ∘ M.mult.η _) ∘ M.M₁ (M.unit.η _) ≡⟨ ap (_∘ M.M₁ (M.unit.η _)) (f .commutes) ⟩ + (M.mult.η _ ∘ M.M₁ (f .morphism)) ∘ M.M₁ (M.unit.η _) ≡˘⟨ assoc (M.mult.η _) (M.M₁ (f .morphism)) (M.M₁ (M.unit.η _)) ⟩ + M.mult.η _ ∘ M.M₁ (f .morphism) ∘ M.M₁ (M.unit.η _) ≡˘⟨ ap (M.mult.η _ ∘_) (M.M-∘ _ _) ⟩ + M.mult.η _ ∘ M.M₁ (f .morphism ∘ M.unit.η _) ≡⟨ ap (λ ϕ → M.mult.η _ ∘ M.M₁ ϕ) p ⟩ + M.mult.η _ ∘ M.M₁ (g .morphism ∘ M.unit.η _) ≡⟨ ap (M.mult.η _ ∘_) (M.M-∘ _ _) ⟩ + M.mult.η _ ∘ M.M₁ (g .morphism) ∘ M.M₁ (M.unit.η _) ≡⟨ assoc (M.mult.η _) (M.M₁ (g .morphism)) (M.M₁ (M.unit.η _)) ⟩ + (M.mult.η _ ∘ M.M₁ (g .morphism)) ∘ M.M₁ (M.unit.η _) ≡˘⟨ ap (_∘ M.M₁ (M.unit.η _)) (g .commutes) ⟩ + (g .morphism ∘ M.mult.η _) ∘ M.M₁ (M.unit.η _) ≡˘⟨ assoc (g .morphism) (M.mult.η _) (M.M₁ (M.unit.η _)) ⟩ + g .morphism ∘ M.mult.η _ ∘ M.M₁ (M.unit.η _) ≡⟨ elimr M.left-ident ⟩ + g .morphism ∎ diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda index 5b158a2..bd751ff 100644 --- a/src/Mugen/Everything.agda +++ b/src/Mugen/Everything.agda @@ -21,6 +21,8 @@ import Mugen.Algebra.OrderedMonoid import Mugen.Cat.Endomorphisms import Mugen.Cat.HierarchyTheory import Mugen.Cat.HierarchyTheory.Properties +import Mugen.Cat.McBrideMonad +import Mugen.Cat.Monad import Mugen.Cat.StrictOrders import Mugen.Data.Int import Mugen.Data.List