From d3ad4c49eb730dc2628acc878615aede56420753 Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 17 May 2024 15:14:01 -0500 Subject: [PATCH] refactor: various improvements for doing Lemma 3.9 --- .../Universality/EndomorphismEmbedding.agda | 157 +++++++++--------- .../EndomorphismEmbeddingNaturality.agda | 79 +++++---- src/Mugen/Cat/Monad.agda | 85 +++++++--- src/Mugen/Cat/StrictOrders.agda | 12 -- src/Mugen/Everything.agda | 1 + src/Mugen/Order/Instances/Copower.agda | 2 +- src/Mugen/Order/Instances/Lift.agda | 18 ++ src/Mugen/Order/Reasoning.agda | 50 +++--- src/Mugen/Order/StrictOrder.agda | 2 +- 9 files changed, 222 insertions(+), 184 deletions(-) create mode 100644 src/Mugen/Order/Instances/Lift.agda diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda index a6bd1fc..a0ba439 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda @@ -31,7 +31,7 @@ import Mugen.Order.Reasoning as Reasoning -- The Universal Embedding Theorem -- Section 3.4, Lemma 3.8 -- --- Given a hierarchy theory 'H', a strict order Δ, and a set Ψ, we can +-- Given a hierarchy theory 'H', a poset Δ, and a set Ψ, we can -- construct a faithful functor 'T : Endos (Fᴴ Δ) → Endos Fᴹᴰ Ψ', where -- 'Fᴴ' denotes the free H-algebra on Δ, and 'Fᴹᴰ Ψ' denotes the free McBride -- Hierarchy theory over the endomorphism displacement algebra on 'H (◆ ⊕ Δ ⊕ Δ)'. @@ -58,7 +58,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding H⟨Δ⁺⟩ : Poset o r H⟨Δ⁺⟩ = H.M₀ Δ⁺ - module H⟨Δ⁺⟩ = Poset H⟨Δ⁺⟩ + module H⟨Δ⁺⟩ = Reasoning H⟨Δ⁺⟩ H⟨Δ⁺⟩→-poset : Poset (lsuc (o ⊔ r)) (o ⊔ r) H⟨Δ⁺⟩→-poset = Endomorphism-poset H Δ⁺ @@ -84,30 +84,34 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→) module SOrdᴹᴰ = Cat SOrdᴹᴰ - Fᴴ⟨_⟩ : Poset o r → Algebra SOrd H - Fᴴ⟨_⟩ = Functor.F₀ (Free SOrd H) + Fᴴ₀ : Poset o r → Algebra SOrd H + Fᴴ₀ = Functor.F₀ (Free SOrd H) + + Fᴴ₁ : {X Y : Poset o r} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y) + Fᴴ₁ = Functor.F₁ (Free SOrd H) Endoᴴ⟨Δ⟩ : Type (o ⊔ r) - Endoᴴ⟨Δ⟩ = Hom (Fᴴ⟨ Δ ⟩ .fst) (Fᴴ⟨ Δ ⟩ .fst) + Endoᴴ⟨Δ⟩ = Hom (H.M₀ Δ) (H.M₀ Δ) - Fᴹᴰ⟨_⟩ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra SOrd↑ (McBride H⟨Δ⁺⟩→) - Fᴹᴰ⟨_⟩ = Functor.F₀ (Free SOrd↑ (McBride H⟨Δ⁺⟩→)) + Fᴹᴰ₀ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra SOrd↑ (McBride H⟨Δ⁺⟩→) + Fᴹᴰ₀ = Functor.F₀ (Free SOrd↑ (McBride H⟨Δ⁺⟩→)) - pattern ⋆ = lift tt - pattern ι₀ α = inl α - pattern ι₁ α = inr (inl α) - pattern ι₂ α = inr (inr α) + -- These patterns and definitions are exported for the naturality proof + -- in another file. - ι₁-inj : ∀ {x y : ⌞ Δ ⌟} → _≡_ {A = ⌞ Δ⁺ ⌟} (ι₁ x) (ι₁ y) → x ≡ y - ι₁-inj = inl-inj ⊙ inr-inj + pattern ⋆ = lift tt - ι₂-inj : ∀ {x y : ⌞ Δ ⌟} → _≡_ {A = ⌞ Δ⁺ ⌟} (ι₂ x) (ι₂ y) → x ≡ y - ι₂-inj = inr-inj ⊙ inr-inj + pattern ι₀ α = inl α ι₀-hom : Hom ◆ Δ⁺ ι₀-hom .hom = ι₀ ι₀-hom .pres-≤[]-equal α≤β = lift α≤β , λ _ → refl + pattern ι₁ α = inr (inl α) + + ι₁-inj : ∀ {x y : ⌞ Δ ⌟} → _≡_ {A = ⌞ Δ⁺ ⌟} (ι₁ x) (ι₁ y) → x ≡ y + ι₁-inj = inl-inj ⊙ inr-inj + ι₁-hom : Hom Δ Δ⁺ ι₁-hom .hom = ι₁ ι₁-hom .pres-≤[]-equal α≤β = lift (lift α≤β) , ι₁-inj @@ -115,21 +119,27 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding ι₁-monic : SOrd.is-monic ι₁-hom ι₁-monic g h p = ext λ α → ι₁-inj (p #ₚ α) + pattern ι₂ α = inr (inr α) + + ι₂-inj : ∀ {x y : ⌞ Δ ⌟} → _≡_ {A = ⌞ Δ⁺ ⌟} (ι₂ x) (ι₂ y) → x ≡ y + ι₂-inj = inr-inj ⊙ inr-inj + -------------------------------------------------------------------------------- -- Construction of the functor T -- Section 3.4, Lemma 3.8 - σ̅ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩ → Hom Δ⁺ H⟨Δ⁺⟩ - σ̅ σ .hom (ι₀ ⋆) = H.unit.η Δ⁺ # ι₀ ⋆ - σ̅ σ .hom (ι₁ α) = H.M₁ ι₁-hom # (σ # (H.unit.η Δ # α)) - σ̅ σ .hom (ι₂ α) = H.unit.η _ # ι₂ α + σ̅ : SOrdᴴ.Hom (Fᴴ₀ Δ) (Fᴴ₀ Δ) → Hom Δ⁺ H⟨Δ⁺⟩ + σ̅ σ .hom (ι₀ ⋆) = H.η Δ⁺ # ι₀ ⋆ + σ̅ σ .hom (ι₁ α) = H.M₁ ι₁-hom # (σ # (H.η Δ # α)) + σ̅ σ .hom (ι₂ α) = H.η Δ⁺ # ι₂ α σ̅ σ .pres-≤[]-equal {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl - σ̅ σ .pres-≤[]-equal {ι₁ α} {ι₁ β} (lift (lift α≤β)) = Σ-map₂ (ap ι₁ ⊙_) $ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ) .pres-≤[]-equal α≤β - σ̅ σ .pres-≤[]-equal {ι₂ α} {ι₂ β} α≤β = H.unit.η Δ⁺ .pres-≤[]-equal α≤β + σ̅ σ .pres-≤[]-equal {ι₁ α} {ι₁ β} (lift (lift α≤β)) = + H⟨Δ⁺⟩.≤[]-map (ap ι₁) $ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) .pres-≤[]-equal α≤β + σ̅ σ .pres-≤[]-equal {ι₂ α} {ι₂ β} α≤β = H.η Δ⁺ .pres-≤[]-equal α≤β abstract - σ̅-id : σ̅ SOrdᴴ.id ≡ H.unit.η Δ⁺ + σ̅-id : σ̅ SOrdᴴ.id ≡ H.η Δ⁺ σ̅-id = ext λ where (ι₀ α) → refl (ι₁ α) → sym (H.unit.is-natural Δ Δ⁺ ι₁-hom) #ₚ α @@ -137,71 +147,56 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding abstract σ̅-ι - : ∀ (σ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) + : ∀ (σ : SOrdᴴ.Hom (Fᴴ₀ Δ) (Fᴴ₀ Δ)) → (α : ⌞ H.M₀ Δ ⌟) - → H.M₁ (H.M₁ ι₁-hom) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # α)) + → H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # α ≡ H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) σ̅-ι σ α = - (H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism) ∘ H.M₁ (H.unit.η Δ)) # α ≡˘⟨ ap (H.M₁ (H.M₁ ι₁-hom) ∘_) (H.M-∘ _ _) #ₚ α ⟩ - (H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism ∘ H.unit.η Δ)) # α ≡˘⟨ H.M-∘ _ _ #ₚ α ⟩ - H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ) # α ≡⟨ ap H.M₁ lemma #ₚ α ⟩ - H.M₁ (σ̅ σ ∘ ι₁-hom) # α ≡⟨ H.M-∘ _ _ #ₚ α ⟩ - H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) ∎ - where - lemma : H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ ≡ σ̅ σ ∘ ι₁-hom - lemma = ext λ _ → refl + H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # α ≡⟨ ap (λ m → H.M₁ m # α) $ ext (λ _ → refl) ⟩ + H.M₁ (σ̅ σ ∘ ι₁-hom) # α ≡⟨ H.M-∘ _ _ #ₚ α ⟩ + H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) ∎ abstract - σ̅-∘ : ∀ (σ δ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → σ̅ (σ SOrdᴴ.∘ δ) ≡ H.mult.η Δ⁺ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ + σ̅-∘ : ∀ (σ δ : SOrdᴴ.Hom (Fᴴ₀ Δ) (Fᴴ₀ Δ)) → σ̅ (σ SOrdᴴ.∘ δ) ≡ H.μ Δ⁺ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ σ̅-∘ σ δ = ext λ where (ι₀ α) → - H.unit.η Δ⁺ # ι₀ α ≡˘⟨ H.right-ident #ₚ (H.unit.η Δ⁺ # ι₀ α) ⟩ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.unit.η Δ⁺ # ι₀ α)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ ι₀ α) ⟩ - H.mult.η Δ⁺ # (H.M₁ (σ̅ σ) # (H.unit.η Δ⁺ # ι₀ α)) ∎ + H.η Δ⁺ # ι₀ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₀ α ⟩ + H.μ Δ⁺ # (H.M₁ (σ̅ σ) # (H.η Δ⁺ # ι₀ α)) ∎ (ι₁ α) → - H.M₁ ι₁-hom # (σ # (δ # (H.unit.η Δ # α))) ≡˘⟨ ap (λ e → H.M₁ ι₁-hom # (σ # e)) (H.left-ident #ₚ _) ⟩ - H.M₁ ι₁-hom # (σ # (H.mult.η Δ # (H.M₁ (H.unit.η Δ) # (δ # (H.unit.η Δ # α))))) ≡⟨ ap# (H.M₁ ι₁-hom) (σ .commutes #ₚ _) ⟩ - H.M₁ ι₁-hom # (H.mult.η _ # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # (δ # (H.unit.η Δ # α))))) ≡˘⟨ H.mult.is-natural _ _ ι₁-hom #ₚ _ ⟩ - H.mult.η _ # (H.M₁ (H.M₁ ι₁-hom) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # (δ # (H.unit.η Δ # α))))) ≡⟨ ap# (H.mult.η _) (σ̅-ι σ (δ # (H.unit.η _ # α))) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # (δ # (H.unit.η Δ # α))) ) ∎ + H.M₁ ι₁-hom # (σ # (δ # (H.η Δ # α))) ≡˘⟨ ap# (H.M₁ ι₁-hom ∘ σ .morphism) $ H.left-ident #ₚ _ ⟩ + H.M₁ ι₁-hom # (σ # (H.μ Δ # (H.M₁ (H.η Δ) # (δ # (H.η Δ # α))))) ≡˘⟨ ap# (H.M₁ ι₁-hom) $ μ-M-∘-Algebraic H σ (H.η Δ) #ₚ _ ⟩ + H.M₁ ι₁-hom # (H.μ _ # (H.M₁ (σ .morphism ∘ H.η Δ) # (δ # (H.η Δ # α)))) ≡˘⟨ μ-M-∘-M H ι₁-hom (σ .morphism ∘ H.η Δ) #ₚ _ ⟩ + H.μ _ # (H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # (δ # (H.η Δ # α))) ≡⟨ ap# (H.μ _) (σ̅-ι σ (δ # (H.η _ # α))) ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # (δ # (H.η Δ # α)))) ∎ (ι₂ α) → - H.unit.η Δ⁺ # ι₂ α ≡˘⟨ H.right-ident #ₚ _ ⟩ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.unit.η Δ⁺ # ι₂ α)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ (ι₂ α)) ⟩ - H.mult.η Δ⁺ # (H.M₁ (σ̅ σ) # (H.unit.η Δ⁺ # ι₂ α)) ∎ - + H.η Δ⁺ # ι₂ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₂ α ⟩ + H.μ Δ⁺ # (H.M₁ (σ̅ σ) # (H.η Δ⁺ # ι₂ α)) ∎ - T′ : (σ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → Algebra-hom SOrd H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩ - T′ σ .morphism = H.mult.η Δ⁺ ∘ H.M₁ (σ̅ σ) + T′ : (σ : SOrdᴴ.Hom (Fᴴ₀ Δ) (Fᴴ₀ Δ)) → SOrdᴴ.Hom (Fᴴ₀ Δ⁺) (Fᴴ₀ Δ⁺) + T′ σ .morphism = H.μ Δ⁺ ∘ H.M₁ (σ̅ σ) T′ σ .commutes = ext λ α → - H.mult.η Δ⁺ # (H.M₁ (σ̅ σ) # (H.mult.η Δ⁺ # α)) ≡˘⟨ ap# (H.mult.η _) (H.mult.is-natural _ _ (σ̅ σ) #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.mult.η (H.M₀ Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ H.mult-assoc #ₚ ((H.M₁ (H.M₁ (σ̅ σ))) # α) ⟩ - H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ ap# (H.mult.η _) (H.M-∘ (H.mult.η _) (H.M₁ (σ̅ σ)) #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺ ∘ H.M₁ (σ̅ σ)) # α) ∎ - - - T : Functor (Endos SOrdᴴ Fᴴ⟨ Δ ⟩) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩) - T = functor - where - functor : Functor (Endos SOrdᴴ Fᴴ⟨ Δ ⟩) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩) - functor .Functor.F₀ _ = tt - functor .Functor.F₁ σ .morphism .hom (α , d) = α , (T′ σ SOrdᴴ.∘ d) - functor .Functor.F₁ σ .morphism .pres-≤[]-equal {α , d1} {β , d2} p = - let d1≤d2 , injr = H⟨Δ⁺⟩→.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 - functor .Functor.F₁ σ .commutes = trivial! - functor .Functor.F-id = ext λ α d → - refl , λ β → - H.mult.η _ # (H.M₁ (σ̅ SOrdᴴ.id) # (d # β)) ≡⟨ ap (λ e → H.mult.η _ # (H.M₁ e # (d # β))) σ̅-id ⟩ - H.mult.η _ # (H.M₁ (H.unit.η _) # (d # β)) ≡⟨ H.left-ident #ₚ _ ⟩ - d # β ∎ - functor .Functor.F-∘ σ δ = ext λ α d → - refl , λ β → - H.mult.η _ # (H.M₁ (σ̅ (σ SOrdᴴ.∘ δ)) # (d # β)) ≡⟨ ap (λ e → H.mult.η _ # (H.M₁ e # (d # β))) (σ̅-∘ σ δ) ⟩ - H.mult.η _ # (H.M₁ (H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # (d # β)) ≡⟨ ap (λ e → H.mult.η _ # (e # (d # β))) (H.M-∘ _ _) ⟩ - H.mult.η _ # ((H.M₁ (H.mult.η _) ∘ H.M₁ (H.M₁ (σ̅ σ) ∘ σ̅ δ)) # (d # β)) ≡⟨ ap (λ e → H.mult.η _ # ((H.M₁ (H.mult.η _) ∘ e) # (d # β))) (H.M-∘ _ _) ⟩ - H.mult.η _ # (H.M₁ (H.mult.η _) # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (σ̅ δ) # (d # β)))) ≡⟨ H.mult-assoc #ₚ _ ⟩ - H.mult.η _ # (H.mult.η _ # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (σ̅ δ) # (d # β)))) ≡⟨ ap# (H.mult.η _) (H.mult.is-natural _ _ (σ̅ σ) #ₚ _) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.mult.η _ # (H.M₁ (σ̅ δ) # (d # β)))) ∎ + H.μ Δ⁺ # (H.M₁ (σ̅ σ) # (H.μ Δ⁺ # α)) ≡˘⟨ ap# (H.μ _) $ H.mult.is-natural _ _ (σ̅ σ) #ₚ α ⟩ + H.μ Δ⁺ # (H.μ (H.M₀ Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ μ-M-∘-μ H (H.M₁ (σ̅ σ)) #ₚ α ⟩ + H.μ Δ⁺ # (H.M₁ (H.μ Δ⁺ ∘ H.M₁ (σ̅ σ)) # α) ∎ + + 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 = + let d1≤d2 , injr = H⟨Δ⁺⟩→.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! + T .Functor.F-id = ext λ α d → + refl , λ β → + H.μ _ # (H.M₁ (σ̅ SOrdᴴ.id) # (d # β)) ≡⟨ ap (λ m → H.μ _ # (H.M₁ m # (d # β))) σ̅-id ⟩ + H.μ _ # (H.M₁ (H.η _) # (d # β)) ≡⟨ H.left-ident #ₚ _ ⟩ + d # β ∎ + T .Functor.F-∘ σ δ = ext λ α d → + refl , λ β → + H.μ _ # (H.M₁ (σ̅ (σ SOrdᴴ.∘ δ)) # (d # β)) ≡⟨ ap (λ m → H.μ _ # (H.M₁ m # (d # β))) (σ̅-∘ σ δ) ⟩ + H.μ _ # (H.M₁ (H.μ _ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # (d # β)) ≡⟨ μ-M-∘-μ H (H.M₁ (σ̅ σ) ∘ σ̅ δ) #ₚ (d # β) ⟩ + H.μ _ # (H.μ _ # (H.M₁ (H.M₁ (σ̅ σ) ∘ σ̅ δ) # (d # β))) ≡⟨ ap# (H.μ _) $ μ-M-∘-M H (σ̅ σ) (σ̅ δ) #ₚ (d # β) ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.μ _ # (H.M₁ (σ̅ δ) # (d # β)))) ∎ -------------------------------------------------------------------------------- -- Faithfulness of T @@ -211,9 +206,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T T-faithful pt H-preserves-monos {x} {y} {σ} {δ} p = 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 _ _ (σ̅ σ) #ₚ _) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.unit.η _ # ι₁ α)) ≡⟨ ap snd (p #ₚ (pt , SOrdᴴ.id)) #ₚ _ ⟩ - H.mult.η _ # (H.M₁ (σ̅ δ) # (H.unit.η _ # ι₁ α)) ≡˘⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ δ) #ₚ _) ⟩ - H.mult.η _ # (H.unit.η _ # (σ̅ δ # (ι₁ α))) ≡⟨ H.right-ident #ₚ _ ⟩ - σ̅ δ # (ι₁ α) ∎ + σ̅ σ # ι₁ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₁ α ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₁ α)) ≡⟨ ap snd (p #ₚ (pt , SOrdᴴ.id)) #ₚ _ ⟩ + H.μ _ # (H.M₁ (σ̅ δ) # (H.η _ # ι₁ α)) ≡⟨ μ-η H (σ̅ δ) #ₚ ι₁ α ⟩ + σ̅ δ # ι₁ α ∎ diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda index 680ba45..fb20ea2 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda @@ -24,6 +24,7 @@ open import Mugen.Cat.HierarchyTheory.McBride open import Mugen.Order.StrictOrder open import Mugen.Order.Instances.Endomorphism renaming (Endomorphism to Endomorphism-poset) open import Mugen.Order.Instances.LeftInvariantRightCentered +open import Mugen.Order.Instances.Lift open import Mugen.Order.Instances.Singleton import Mugen.Order.Reasoning as Reasoning @@ -65,7 +66,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality H⟨Δ⁺⟩ : Poset o r H⟨Δ⁺⟩ = H.M₀ Δ⁺ - module H⟨Δ⁺⟩ = Poset H⟨Δ⁺⟩ + module H⟨Δ⁺⟩ = Reasoning H⟨Δ⁺⟩ H⟨Δ⁺⟩→-poset : Poset (lsuc (o ⊔ r)) (o ⊔ r) H⟨Δ⁺⟩→-poset = Endomorphism-poset H Δ⁺ @@ -91,8 +92,11 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→) module SOrdᴹᴰ = Cat SOrdᴹᴰ - Fᴴ⟨_⟩ : Poset o r → Algebra SOrd H - Fᴴ⟨_⟩ = Functor.F₀ (Free SOrd H) + Fᴴ₀ : Poset o r → Algebra SOrd H + Fᴴ₀ = Functor.F₀ (Free SOrd H) + + Fᴴ₁ : {X Y : Poset o r} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y) + Fᴴ₁ = Functor.F₁ (Free SOrd H) -------------------------------------------------------------------------------- -- NOTE: Forgetful Functors + Levels @@ -124,11 +128,11 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality where ℓ̅ : ⌞ H.M₀ Δ ⌟ → Hom Δ⁺ (H.M₀ Δ⁺) ℓ̅ ℓ .hom (ι₀ _) = H.M₁ ι₁-hom # ℓ - ℓ̅ ℓ .hom (ι₁ α) = H.unit.η _ # ι₂ α - ℓ̅ ℓ .hom (ι₂ α) = H.unit.η _ # ι₂ α + ℓ̅ ℓ .hom (ι₁ α) = H.η _ # ι₂ α + ℓ̅ ℓ .hom (ι₂ α) = H.η _ # ι₂ α ℓ̅ ℓ .pres-≤[]-equal {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl - ℓ̅ ℓ .pres-≤[]-equal {ι₁ α} {ι₁ β} α≤β = Σ-map₂ ((ap ι₁ ⊙ ι₂-inj) ⊙_) $ H.unit.η _ .pres-≤[]-equal α≤β - ℓ̅ ℓ .pres-≤[]-equal {ι₂ α} {ι₂ β} α≤β = H.unit.η _ .pres-≤[]-equal α≤β + ℓ̅ ℓ .pres-≤[]-equal {ι₁ α} {ι₁ β} α≤β = H⟨Δ⁺⟩.≤[]-map (ap ι₁ ⊙ ι₂-inj) $ H.η _ .pres-≤[]-equal α≤β + ℓ̅ ℓ .pres-≤[]-equal {ι₂ α} {ι₂ β} α≤β = H.η _ .pres-≤[]-equal α≤β abstract ℓ̅-pres-≤ : ∀ {ℓ ℓ′} @@ -138,49 +142,46 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality ℓ̅-pres-≤ ℓ′≤ℓ (ι₁ _) = H⟨Δ⁺⟩.≤-refl ℓ̅-pres-≤ ℓ′≤ℓ (ι₂ _) = H⟨Δ⁺⟩.≤-refl - ν′ : ⌞ H.M₀ Δ ⌟ → Algebra-hom SOrd H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩ - ν′ ℓ .morphism = H.mult.η Δ⁺ ∘ H.M₁ (ℓ̅ ℓ) + ν′ : ⌞ H.M₀ Δ ⌟ → SOrdᴴ.Hom (Fᴴ₀ Δ⁺) (Fᴴ₀ Δ⁺) + ν′ ℓ .morphism = H.μ Δ⁺ ∘ H.M₁ (ℓ̅ ℓ) ν′ ℓ .commutes = ext λ α → - H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.mult.η Δ⁺ # α)) ≡˘⟨ ap# (H.mult.η _) (H.mult.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.mult.η (H.M₀ Δ⁺) # (H.M₁ (H.M₁ (ℓ̅ ℓ)) # α)) ≡˘⟨ H.mult-assoc #ₚ _ ⟩ - H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺) # (H.M₁ (H.M₁ (ℓ̅ ℓ)) # α)) ≡˘⟨ ap# (H.mult.η _) (H.M-∘ _ _ #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺ ∘ H.M₁ (ℓ̅ ℓ)) # α) ∎ + H.μ Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.μ Δ⁺ # α)) ≡˘⟨ ap# (H.μ _) (H.mult.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ + H.μ Δ⁺ # (H.μ (H.M₀ Δ⁺) # (H.M₁ (H.M₁ (ℓ̅ ℓ)) # α)) ≡˘⟨ μ-M-∘-μ H (H.M₁ (ℓ̅ ℓ)) #ₚ α ⟩ + H.μ Δ⁺ # (H.M₁ (H.μ Δ⁺ ∘ H.M₁ (ℓ̅ ℓ)) # α) ∎ abstract ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→-poset.≤ ν′ ℓ ν′-mono {ℓ′} {ℓ} ℓ′≤ℓ α = begin-≤ - H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η Δ⁺ # α)) ≐⟨ ap# (H.mult.η _) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (ℓ̅ ℓ′ # α)) ≤⟨ pres-≤ (H.mult.η _ ∘ H.unit.η _) (ℓ̅-pres-≤ ℓ′≤ℓ α) ⟩ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (ℓ̅ ℓ # α)) ≐⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η Δ⁺ # α)) ≤∎ + H.μ Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.η Δ⁺ # α)) ≐⟨ μ-η H (ℓ̅ ℓ′) #ₚ α ⟩ + ℓ̅ ℓ′ # α ≤⟨ ℓ̅-pres-≤ ℓ′≤ℓ α ⟩ + ℓ̅ ℓ # α ≐⟨ sym $ μ-η H (ℓ̅ ℓ) #ₚ α ⟩ + H.μ Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.η Δ⁺ # α)) ≤∎ where open Reasoning (H.M₀ Δ⁺) abstract ν′-injective-on-related : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ ≡ ν′ ℓ → ℓ′ ≡ ℓ - ν′-injective-on-related {ℓ′} {ℓ} ℓ′≤ℓ p = injective-on-related (H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom) ℓ′≤ℓ $ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.M₁ ι₁-hom # ℓ′)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ _) ⟩ - H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η Δ⁺ # ι₀ ⋆)) ≡⟨ p #ₚ (H.unit.η _ # ι₀ ⋆) ⟩ - H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η Δ⁺ # ι₀ ⋆)) ≡˘⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ _) ⟩ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.M₁ ι₁-hom # ℓ)) ∎ + ν′-injective-on-related {ℓ′} {ℓ} ℓ′≤ℓ p = injective-on-related (H.M₁ ι₁-hom) ℓ′≤ℓ $ + H.M₁ ι₁-hom # ℓ′ ≡˘⟨ μ-η H (ℓ̅ ℓ′) #ₚ _ ⟩ + H.μ Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.η Δ⁺ # ι₀ ⋆)) ≡⟨ p #ₚ (H.η _ # ι₀ ⋆) ⟩ + H.μ Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.η Δ⁺ # ι₀ ⋆)) ≡⟨ μ-η H (ℓ̅ ℓ) #ₚ _ ⟩ + H.M₁ ι₁-hom # ℓ ∎ abstract - ℓ̅-σ̅ : ∀ {ℓ : ⌞ Fᴴ⟨ Δ ⟩ ⌟} (σ : Algebra-hom _ _ Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → ℓ̅ (σ # ℓ) ≡ H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ + ℓ̅-σ̅ : ∀ {ℓ : ⌞ Fᴴ₀ Δ ⌟} (σ : SOrdᴴ.Hom (Fᴴ₀ Δ) (Fᴴ₀ Δ)) → ℓ̅ (σ # ℓ) ≡ H.μ _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ ℓ̅-σ̅ {ℓ} σ = ext λ where (ι₀ ⋆) → - H.M₁ ι₁-hom # (σ # ℓ) ≡˘⟨ ap (λ e → H.M₁ ι₁-hom # (σ # e)) (H.left-ident #ₚ ℓ) ⟩ - H.M₁ ι₁-hom # (σ # (H.mult.η _ # (H.M₁ (H.unit.η _) # ℓ))) ≡⟨ ap# (H.M₁ ι₁-hom) (σ .commutes #ₚ _) ⟩ - H.M₁ ι₁-hom # (H.mult.η _ # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η _) # ℓ))) ≡˘⟨ H.mult.is-natural _ _ ι₁-hom #ₚ _ ⟩ - H.mult.η _ # (H.M₁ (H.M₁ ι₁-hom) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # ℓ))) ≡⟨ ap# (H.mult.η _) (σ̅-ι σ ℓ) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # ℓ)) ∎ + H.M₁ ι₁-hom # (σ # ℓ) ≡˘⟨ ap# (H.M₁ ι₁-hom ∘ σ .morphism) $ H.left-ident #ₚ ℓ ⟩ + H.M₁ ι₁-hom # (σ # (H.μ _ # (H.M₁ (H.η _) # ℓ))) ≡˘⟨ ap# (H.M₁ ι₁-hom) $ μ-M-∘-Algebraic H σ (H.η Δ) #ₚ _ ⟩ + H.M₁ ι₁-hom # (H.μ _ # (H.M₁ (σ .morphism ∘ H.η _) # ℓ)) ≡˘⟨ μ-M-∘-M H ι₁-hom (σ .morphism ∘ H.η Δ) #ₚ _ ⟩ + H.μ _ # (H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # ℓ) ≡⟨ ap# (H.μ _) (σ̅-ι σ ℓ) ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # ℓ)) ∎ (ι₁ α) → - H.unit.η _ # ι₂ α ≡˘⟨ H.right-ident #ₚ _ ⟩ - H.mult.η _ # (H.unit.η _ # (H.unit.η _ # ι₂ α)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ (ι₂ α)) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.unit.η _ # ι₂ α)) ∎ + H.η _ # ι₂ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ _ ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₂ α)) ∎ (ι₂ α) → - H.unit.η _ # ι₂ α ≡˘⟨ H.right-ident #ₚ _ ⟩ - H.mult.η _ # (H.unit.η _ # (H.unit.η _ # ι₂ α)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ (ι₂ α)) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.unit.η _ # ι₂ α)) ∎ + H.η _ # ι₂ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ _ ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₂ α)) ∎ nt : Uᴴ => Uᴹᴰ F∘ T nt ._=>_.η _ .hom (lift ℓ) = pt , ν′ ℓ @@ -188,9 +189,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality inc (biased refl (ν′-mono ℓ≤ℓ′)) , λ p → ap lift $ ν′-injective-on-related ℓ≤ℓ′ (ap snd p) nt ._=>_.is-natural _ _ σ = ext λ ℓ → refl , λ α → - H.mult.η _ # (H.M₁ (ℓ̅ (σ # ℓ)) # α) ≡⟨ ap (λ e → (H.mult.η _ ∘ H.M₁ e) # α) (ℓ̅-σ̅ σ) ⟩ - H.mult.η _ # (H.M₁ (H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ) # α) ≡⟨ ap# (H.mult.η _) (H.M-∘ _ _ #ₚ α) ⟩ - H.mult.η _ # ((H.M₁ (H.mult.η _) ∘ H.M₁ (H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ)) # α) ≡⟨ ap (λ e → H.mult.η _ # ((H.M₁ (H.mult.η _) ∘ e) # α)) (H.M-∘ (H.M₁ (σ̅ σ)) (ℓ̅ ℓ)) ⟩ - H.mult.η _ # (H.M₁ (H.mult.η _) # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (ℓ̅ ℓ) # α))) ≡⟨ H.mult-assoc #ₚ _ ⟩ - H.mult.η _ # (H.mult.η _ # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (ℓ̅ ℓ) # α))) ≡⟨ ap# (H.mult.η _) (H.mult.is-natural _ _ (σ̅ σ) #ₚ _) ⟩ - H.mult.η _ # (H.M₁ (σ̅ σ) # (H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # α))) ∎ + H.μ _ # (H.M₁ (ℓ̅ (σ # ℓ)) # α) ≡⟨ ap (λ m → (H.μ _ ∘ H.M₁ m) # α) (ℓ̅-σ̅ σ) ⟩ + H.μ _ # (H.M₁ (H.μ _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ) # α) ≡⟨ μ-M-∘-μ H (H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ) #ₚ α ⟩ + H.μ _ # (H.μ _ # (H.M₁ (H.M₁ (σ̅ σ) ∘ (ℓ̅ ℓ)) # α)) ≡⟨ ap# (H.μ _) $ μ-M-∘-M H (σ̅ σ) (ℓ̅ ℓ) #ₚ α ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.μ _ # (H.M₁ (ℓ̅ ℓ) # α))) ∎ diff --git a/src/Mugen/Cat/Monad.agda b/src/Mugen/Cat/Monad.agda index 592a887..eac5899 100644 --- a/src/Mugen/Cat/Monad.agda +++ b/src/Mugen/Cat/Monad.agda @@ -15,26 +15,65 @@ module _ {o r} {C : Precategory o r} (M : Monad C) where 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 ∎ + Free₀ : Ob → Algebra C M + Free₀ = Functor.F₀ (Free C M) + + Free₁ : ∀ {X Y} → Hom X Y → Algebra-hom C M (Free₀ X) (Free₀ Y) + Free₁ = Functor.F₁ (Free C M) + + abstract + μ-M-∘-Algebraic : ∀ {X Y Z} (σ : Algebra-hom C M (Free₀ Y) (Free₀ Z)) (δ : Hom X (M.M₀ Y)) + → M.μ Z ∘ M.M₁ (σ .morphism ∘ δ) ≡ σ .morphism ∘ M.μ Y ∘ M.M₁ δ + μ-M-∘-Algebraic {X = X} {Y} {Z} σ δ = + M.μ Z ∘ M.M₁ (σ .morphism ∘ δ) + ≡⟨ ap (M.μ Z ∘_) $ M.M-∘ (σ .morphism) δ ⟩ + M.μ Z ∘ M.M₁ (σ .morphism) ∘ (M.M₁ δ) + ≡⟨ assoc (M.μ Z) (M.M₁ (σ .morphism)) (M.M₁ δ) ⟩ + (M.μ Z ∘ M.M₁ (σ .morphism)) ∘ (M.M₁ δ) + ≡˘⟨ ap (_∘ M.M₁ δ) $ σ .commutes ⟩ + (σ .morphism ∘ M.μ Y) ∘ M.M₁ δ + ≡˘⟨ assoc (σ .morphism) (M.μ Y) (M.M₁ δ) ⟩ + σ .morphism ∘ M.μ Y ∘ M.M₁ δ + ∎ + + μ-M-∘-M : ∀ {X Y Z} (σ : Hom Y Z) (δ : Hom X (M.M₀ Y)) + → M.μ Z ∘ M.M₁ (M.M₁ σ ∘ δ) ≡ M.M₁ σ ∘ M.μ Y ∘ M.M₁ δ + μ-M-∘-M σ δ = μ-M-∘-Algebraic (Free₁ σ) δ + + μ-M-∘-μ : ∀ {X Y} (σ : Hom X (M.M₀ (M.M₀ Y))) + → M.μ Y ∘ M.M₁ (M.μ Y ∘ σ) ≡ M.μ Y ∘ M.μ (M.M₀ Y) ∘ M.M₁ σ + μ-M-∘-μ {Y = Y} σ = + M.μ Y ∘ M.M₁ (M.μ Y ∘ σ) + ≡⟨ ap (M.μ Y ∘_) $ M.M-∘ (M.μ Y) σ ⟩ + M.μ Y ∘ M.M₁ (M.μ Y) ∘ M.M₁ σ + ≡⟨ assoc (M.μ Y) (M.M₁ (M.μ Y)) (M.M₁ σ) ⟩ + (M.μ Y ∘ M.M₁ (M.μ Y)) ∘ M.M₁ σ + ≡⟨ ap (_∘ M.M₁ σ) $ M.mult-assoc ⟩ + (M.μ Y ∘ M.μ (M.M₀ Y)) ∘ M.M₁ σ + ≡˘⟨ assoc (M.μ Y) (M.μ (M.M₀ Y)) (M.M₁ σ) ⟩ + M.μ Y ∘ M.μ (M.M₀ Y) ∘ M.M₁ σ + ∎ + + -- Favonia: what would be a better name? + μ-η : ∀ {X Y} (σ : Hom X (M.M₀ Y)) + → M.μ Y ∘ M.M₁ σ ∘ M.η X ≡ σ + μ-η {X = X} {Y} σ = + M.μ Y ∘ M.M₁ σ ∘ M.η X + ≡˘⟨ ap (M.μ Y ∘_) $ M.unit.is-natural X (M.M₀ Y) σ ⟩ + M.μ Y ∘ M.η (M.M₀ Y) ∘ σ + ≡⟨ assoc (M.μ Y) (M.η (M.M₀ Y)) σ ⟩ + (M.μ Y ∘ M.η (M.M₀ Y)) ∘ σ + ≡⟨ eliml M.right-ident ⟩ + σ + ∎ + + -- Favonia: does this lemma belong to 1lab? + free-algebra-hom-path : ∀ {X Y} {f g : Algebra-hom C M (Free₀ X) (Free₀ Y)} + → f .morphism ∘ M.η _ ≡ (g .morphism ∘ M.η _) → f ≡ g + free-algebra-hom-path {f = f} {g = g} p = Algebra-hom-path _ $ + f .morphism ≡⟨ intror M.left-ident ⟩ + f .morphism ∘ M.μ _ ∘ M.M₁ (M.η _) ≡˘⟨ μ-M-∘-Algebraic f (M.η _) ⟩ + M.μ _ ∘ M.M₁ (f .morphism ∘ M.η _) ≡⟨ ap (λ ϕ → M.μ _ ∘ M.M₁ ϕ) p ⟩ + M.μ _ ∘ M.M₁ (g .morphism ∘ M.η _) ≡⟨ μ-M-∘-Algebraic g (M.η _) ⟩ + g .morphism ∘ M.μ _ ∘ M.M₁ (M.η _) ≡⟨ elimr M.left-ident ⟩ + g .morphism ∎ diff --git a/src/Mugen/Cat/StrictOrders.agda b/src/Mugen/Cat/StrictOrders.agda index 1039518..5ff2cef 100644 --- a/src/Mugen/Cat/StrictOrders.agda +++ b/src/Mugen/Cat/StrictOrders.agda @@ -21,15 +21,3 @@ Strict-orders o r ._∘_ = strictly-monotone-∘ Strict-orders o r .idr f = ext λ _ → refl Strict-orders o r .idl f = ext λ _ → refl Strict-orders o r .assoc f g h = ext λ _ → refl - -Lift≤ - : ∀ {o r} - → (o′ r′ : Level) - → Poset o r - → Poset (o ⊔ o′) (r ⊔ r′) -Lift≤ o' r' X .Poset.Ob = Lift o' ⌞ X ⌟ -Lift≤ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (Lift.lower x) (Lift.lower y) -Lift≤ o' r' X .Poset.≤-thin = Lift-is-hlevel 1 $ X .Poset.≤-thin -Lift≤ o' r' X .Poset.≤-refl = lift $ X .Poset.≤-refl -Lift≤ o' r' X .Poset.≤-trans (lift p) (lift q) = lift (X .Poset.≤-trans p q) -Lift≤ o' r' X .Poset.≤-antisym (lift p) (lift q) = ap lift (X .Poset.≤-antisym p q) diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda index b485732..e8530c9 100644 --- a/src/Mugen/Everything.agda +++ b/src/Mugen/Everything.agda @@ -36,6 +36,7 @@ import Mugen.Order.Instances.Fractal import Mugen.Order.Instances.Int import Mugen.Order.Instances.LeftInvariantRightCentered import Mugen.Order.Instances.Lexicographic +import Mugen.Order.Instances.Lift import Mugen.Order.Instances.Nat import Mugen.Order.Instances.NonPositive import Mugen.Order.Instances.Opposite diff --git a/src/Mugen/Order/Instances/Copower.agda b/src/Mugen/Order/Instances/Copower.agda index 28c38d6..0af6c05 100644 --- a/src/Mugen/Order/Instances/Copower.agda +++ b/src/Mugen/Order/Instances/Copower.agda @@ -6,4 +6,4 @@ open import Mugen.Prelude open import Mugen.Order.Instances.Product Copower : ∀ {o o' r'} → Set o → Poset o' r' → Poset (o ⊔ o') (o ⊔ r') -Copower I A = Product (Disc I) A +Copower I A = Product (Discᵢ I) A diff --git a/src/Mugen/Order/Instances/Lift.agda b/src/Mugen/Order/Instances/Lift.agda new file mode 100644 index 0000000..58368ca --- /dev/null +++ b/src/Mugen/Order/Instances/Lift.agda @@ -0,0 +1,18 @@ +open import Mugen.Prelude + +module Mugen.Order.Instances.Lift where + +private variable + o r : Level + +Lift≤ + : ∀ {o r} + → (o′ r′ : Level) + → Poset o r + → Poset (o ⊔ o′) (r ⊔ r′) +Lift≤ o' r' X .Poset.Ob = Lift o' ⌞ X ⌟ +Lift≤ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (Lift.lower x) (Lift.lower y) +Lift≤ o' r' X .Poset.≤-thin = Lift-is-hlevel 1 $ X .Poset.≤-thin +Lift≤ o' r' X .Poset.≤-refl = lift $ X .Poset.≤-refl +Lift≤ o' r' X .Poset.≤-trans (lift p) (lift q) = lift (X .Poset.≤-trans p q) +Lift≤ o' r' X .Poset.≤-antisym (lift p) (lift q) = ap lift (X .Poset.≤-antisym p q) diff --git a/src/Mugen/Order/Reasoning.agda b/src/Mugen/Order/Reasoning.agda index 0112061..328185e 100644 --- a/src/Mugen/Order/Reasoning.agda +++ b/src/Mugen/Order/Reasoning.agda @@ -41,14 +41,18 @@ module Mugen.Order.Reasoning {o r} (A : Poset o r) where ≤[]-is-hlevel n hb = ×-is-hlevel (1 + n) (is-prop→is-hlevel-suc ≤-thin) $ Π-is-hlevel (1 + n) λ _ → hb + -- This overlaps with the H-Level instance for Σ {- - instance + abstract instance H-Level-≤[] : ∀ {r'} {K : Type r'} {n k : Nat} {x y} → ⦃ H-Level K (1 + n) ⦄ → H-Level (x ≤[ K ] y) (1 + n + k) H-Level-≤[] {n = n} ⦃ hb ⦄ = basic-instance (1 + n) $ ≤[]-is-hlevel n (hb .H-Level.has-hlevel) -} + ≤[]-map : ∀ {x y} {K : Type r'} {K' : Type r''} → (K → K') → x ≤[ K ] y → x ≤[ K' ] y + ≤[]-map f p = Σ-map₂ (f ⊙_) p + _<_ : Ob → Ob → Type (o ⊔ r) x < y = x ≤[ ⊥ ] y @@ -66,7 +70,7 @@ module Mugen.Order.Reasoning {o r} (A : Poset o r) where y