From 0a704404667427b7e803c08313141aa04e7520dd Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 7 Nov 2023 20:19:27 -0500 Subject: [PATCH] Cleanup code, bring up to date with new versions of 1Lab and Agda (#21) --- Dockerfile | 6 +- agda-mugen.agda-lib | 4 +- src/Mugen/Algebra/Displacement.agda | 427 +++++++++++++----- src/Mugen/Algebra/Displacement/Coimage.agda | 232 ++++------ src/Mugen/Algebra/Displacement/Constant.agda | 95 ++-- .../Algebra/Displacement/Endomorphism.agda | 96 ++-- .../Algebra/Displacement/FiniteSupport.agda | 102 +++-- src/Mugen/Algebra/Displacement/Fractal.agda | 68 ++- .../Algebra/Displacement/InfiniteProduct.agda | 90 ++-- src/Mugen/Algebra/Displacement/Int.agda | 39 +- .../Algebra/Displacement/Lexicographic.agda | 92 ++-- src/Mugen/Algebra/Displacement/Nat.agda | 42 +- .../Algebra/Displacement/NearlyConstant.agda | 262 ++++++----- .../Algebra/Displacement/NonPositive.agda | 34 +- src/Mugen/Algebra/Displacement/Opposite.agda | 58 +-- src/Mugen/Algebra/Displacement/Prefix.agda | 37 +- src/Mugen/Algebra/Displacement/Product.agda | 105 +++-- src/Mugen/Algebra/OrderedMonoid.agda | 87 ++-- src/Mugen/Axioms/LPO.agda | 14 +- src/Mugen/Cat/HierarchyTheory.agda | 88 ++-- src/Mugen/Cat/HierarchyTheory/Properties.agda | 323 +++++++------ src/Mugen/Cat/StrictOrders.agda | 61 +-- src/Mugen/Data/Int.agda | 135 +++--- src/Mugen/Data/List.agda | 6 +- src/Mugen/Data/Nat.agda | 155 ++----- src/Mugen/Data/NonEmpty.agda | 6 +- src/Mugen/Everything.agda | 6 +- src/Mugen/Order/Coproduct.agda | 124 ++--- src/Mugen/Order/Discrete.agda | 15 +- src/Mugen/Order/InfiniteCoproduct.agda | 22 - .../Order/LeftInvariantRightCentered.agda | 157 ++++--- src/Mugen/Order/Opposite.agda | 35 +- src/Mugen/Order/PartialOrder.agda | 29 -- src/Mugen/Order/Poset.agda | 81 ++-- src/Mugen/Order/Prefix.agda | 12 +- src/Mugen/Order/Prelude.agda | 19 - src/Mugen/Order/Product.agda | 22 - src/Mugen/Order/Singleton.agda | 15 +- src/Mugen/Order/StrictOrder.agda | 325 ++++++------- src/Mugen/Order/StrictOrder/Coimage.agda | 114 +++++ src/Mugen/Order/StrictOrder/Reasoning.agda | 50 ++ src/Mugen/Prelude.agda | 94 +--- 42 files changed, 1968 insertions(+), 1816 deletions(-) delete mode 100644 src/Mugen/Order/InfiniteCoproduct.agda delete mode 100644 src/Mugen/Order/PartialOrder.agda delete mode 100644 src/Mugen/Order/Prelude.agda delete mode 100644 src/Mugen/Order/Product.agda create mode 100644 src/Mugen/Order/StrictOrder/Coimage.agda create mode 100644 src/Mugen/Order/StrictOrder/Reasoning.agda diff --git a/Dockerfile b/Dockerfile index 4f7d951..1b9bf69 100644 --- a/Dockerfile +++ b/Dockerfile @@ -2,13 +2,13 @@ # Stage 1: building everything except agda-mugen #################################################################################################### -FROM fossa/haskell-static-alpine:ghc-9.0.2 AS agda +FROM fossa/haskell-static-alpine:ghc-9.4.7 AS agda WORKDIR /build/agda RUN \ git init && \ git remote add origin https://github.com/agda/agda.git && \ - git fetch --depth 1 origin efa6fe4cc65132bcc375f608542154674a37f1ba && \ + git fetch --depth 1 origin 5c8116227e2d9120267aed43f0e545a65d9c2fe2 && \ git checkout FETCH_HEAD # We build Agda and place it in /dist along with its data files. @@ -36,7 +36,7 @@ WORKDIR /dist/1lab RUN \ git init && \ git remote add origin https://github.com/plt-amy/1lab && \ - git fetch --depth 1 origin f5465e947501f971bd2dfb76915e4065b13194c5 && \ + git fetch --depth 1 origin ac6f81089a261e9c0d2ce3ede37a4a09764cb2ad && \ git checkout FETCH_HEAD RUN echo "/dist/1lab/1lab.agda-lib" > /dist/libraries diff --git a/agda-mugen.agda-lib b/agda-mugen.agda-lib index 7d2f01d..afe74c4 100644 --- a/agda-mugen.agda-lib +++ b/agda-mugen.agda-lib @@ -1,5 +1,5 @@ name: agda-mugen -depend: cubical-1lab +depend: 1lab include: src wip @@ -9,4 +9,4 @@ flags: --postfix-projections --rewriting --guardedness - -W noNoEquivWhenSplitting \ No newline at end of file + -WnoUnsupportedIndexedMatch \ No newline at end of file diff --git a/src/Mugen/Algebra/Displacement.agda b/src/Mugen/Algebra/Displacement.agda index 4aa7c37..9be6398 100644 --- a/src/Mugen/Algebra/Displacement.agda +++ b/src/Mugen/Algebra/Displacement.agda @@ -12,161 +12,219 @@ import Mugen.Data.Nat as Nat private variable - o r : Level + o r o' r' : Level A : Type o -------------------------------------------------------------------------------- -- Displacement Algebras +-- +-- Like ordered monoids, we view displacement algebras as structures +-- over an order. -record is-displacement-algebra {A : Type o} (_<_ : A → A → Type r) (ε : A) (_⊗_ : A → A → A) : Type (o ⊔ r) where +record is-displacement-algebra + {o r} (A : Strict-order o r) + (ε : ⌞ A ⌟) (_⊗_ : ⌞ A ⌟ → ⌞ A ⌟ → ⌞ A ⌟) + : Type (o ⊔ r) + where + no-eta-equality + open Strict-order A field - has-monoid : is-monoid ε _⊗_ - has-strict-order : is-strict-order _<_ + has-is-monoid : is-monoid ε _⊗_ left-invariant : ∀ {x y z} → y < z → (x ⊗ y) < (x ⊗ z) - open is-monoid has-monoid public - open is-strict-order has-strict-order public renaming (has-prop to <-is-prop) + open is-monoid has-is-monoid hiding (has-is-set) public left-invariant-≤ : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤ (x ⊗ z) left-invariant-≤ {x = x} (inl p) = inl (ap (x ⊗_) p) left-invariant-≤ (inr y_ + -------------------------------------------------------------------------------- -- Heirarchy Theories -- -- A heirarchy theory is defined to be a monad on the category of strict orders. -- We also define the McBride Heirarchy Theory. -HierarchyTheory : ∀ o r → Type (lsuc o ⊔ lsuc r) -HierarchyTheory o r = Monad (StrictOrders o r) +Hierarchy-theory : ∀ o r → Type (lsuc o ⊔ lsuc r) +Hierarchy-theory o r = Monad (Strict-orders o r) -------------------------------------------------------------------------------- -- The McBride Hierarchy Theory @@ -27,28 +31,28 @@ HierarchyTheory o r = Monad (StrictOrders o r) -- -- A construction of the McBride Monad for any displacement algebra '𝒟' -ℳ : ∀ {o} → DisplacementAlgebra o o → HierarchyTheory o o +ℳ : ∀ {o} → Displacement-algebra o o → Hierarchy-theory o o ℳ {o = o} 𝒟 = ht where - open DisplacementAlgebra-on (structure 𝒟) - - M : Functor (StrictOrders o o) (StrictOrders o o) - M .Functor.F₀ L = L ⋉ (DA→SO 𝒟) [ ε ] - M .Functor.F₁ f ⟨$⟩ (l , d) = (f ⟨$⟩ l) , d - M .Functor.F₁ f .homo x M - unit ._=>_.η L ⟨$⟩ l = l , ε - unit ._=>_.η L .homo l_.is-natural L L′ f = strict-order-path λ _ → refl + unit .η L .hom l = l , ε + unit .η L .strict-mono l M - mult ._=>_.η L ⟨$⟩ ((l , x) , y) = l , (x ⊗ y) - mult ._=>_.η L .homo {(α , d1) , d2} {(β , e1) , e2} l_.is-natural L L' f = strict-order-path λ _ → refl + mult .is-natural L L' f = trivial! - ht : HierarchyTheory o o + ht : Hierarchy-theory o o ht .Monad.M = M ht .Monad.unit = unit ht .Monad.mult = mult - ht .Monad.left-ident = strict-order-path λ where - (α , d) i → (α , idl {d} i) - ht .Monad.right-ident = strict-order-path λ where - (α , d) i → (α , idr {d} i) - ht .Monad.mult-assoc = strict-order-path λ where - (((α , d1) , d2) , d3) i → α , associative {d1} {d2} {d3} (~ i) + 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 : HierarchyTheory o r} where +module _ {o r} {H : Hierarchy-theory o r} where private module H = Monad H - Free⟨_⟩ : StrictOrder o r → Algebra (StrictOrders o r) H - Free⟨_⟩ = Functor.F₀ (Free (StrictOrders o r) H) + Free⟨_⟩ : Strict-order o r → Algebra (Strict-orders o r) H + Free⟨_⟩ = Functor.F₀ (Free (Strict-orders o r) H) - open Cat (StrictOrders o r) + open Cat (Strict-orders o r) open Algebra-hom - hierarchy-algebra-path : ∀ {X Y} {f g : Algebra-hom (StrictOrders o r) H X Y} - → (∀ α → f .morphism ⟨$⟩ α ≡ g .morphism ⟨$⟩ α) - → f ≡ g - hierarchy-algebra-path p = Algebra-hom-path _ (strict-order-path p) - - hierarchy-algebra-happly : ∀ {X Y} {f g : Algebra-hom (StrictOrders o r) H X Y} - → f ≡ g - → (∀ α → f .morphism ⟨$⟩ α ≡ g .morphism ⟨$⟩ α) - hierarchy-algebra-happly p α i = p i .morphism ⟨$⟩ α - -- 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-path : ∀ {X Y} {f g : Algebra-hom (StrictOrders o r) H Free⟨ X ⟩ Free⟨ Y ⟩} + free-algebra-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-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.η _) ≡⟨ 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.η _) ≡˘⟨ 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.η _) ≡⟨ 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.η _) ≡˘⟨ 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 -preserves-monos : ∀ {o r} (H : HierarchyTheory o r) → Type (lsuc o ⊔ lsuc r) +preserves-monos : ∀ {o r} (H : Hierarchy-theory o r) → Type (lsuc o ⊔ lsuc r) preserves-monos {o} {r} H = ∀ {X Y} → (f : Hom X Y) → is-monic f → is-monic (H.M₁ f) where module H = Monad H - open Cat (StrictOrders o r) + open Cat (Strict-orders o r) diff --git a/src/Mugen/Cat/HierarchyTheory/Properties.agda b/src/Mugen/Cat/HierarchyTheory/Properties.agda index a01301a..a8af376 100644 --- a/src/Mugen/Cat/HierarchyTheory/Properties.agda +++ b/src/Mugen/Cat/HierarchyTheory/Properties.agda @@ -1,8 +1,8 @@ -{-# OPTIONS --experimental-lossy-unification #-} module Mugen.Cat.HierarchyTheory.Properties where open import Cat.Prelude open import Cat.Functor.Base +open import Cat.Functor.Properties open import Cat.Diagram.Monad import Cat.Reasoning as Cat @@ -23,6 +23,8 @@ open import Mugen.Order.StrictOrder open import Mugen.Order.Singleton open import Mugen.Order.Discrete +import Mugen.Order.StrictOrder.Reasoning + -------------------------------------------------------------------------------- -- The Universal Embedding Theorem -- Section 3.4, Lemma 3.8 @@ -32,8 +34,10 @@ open import Mugen.Order.Discrete -- 'Fᴴ' denotes the free H-algebra on Δ, and 'Fᴹᴰ Ψ' denotes the free McBride -- Heirarchy theory over the endomorphism displacement algebra on 'H (◆ ⊕ Δ ⊕ Δ)'. -module _ {o r} (H : HierarchyTheory o r) (Δ : StrictOrder o r) (Ψ : Set (lsuc o ⊔ lsuc r)) where +module _ {o r} (H : Hierarchy-theory o r) (Δ : Strict-order o r) (Ψ : Set (lsuc o ⊔ lsuc r)) where + open Strictly-monotone open Algebra-hom + open Cat (Strict-orders o r) -------------------------------------------------------------------------------- -- Notation @@ -41,11 +45,11 @@ module _ {o r} (H : HierarchyTheory o r) (Δ : StrictOrder o r) (Ψ : Set (lsuc -- We begin by defining some useful notation. private - Δ⁺ : StrictOrder o r + Δ⁺ : Strict-order o r Δ⁺ = ◆ ⊕ (Δ ⊕ Δ) - 𝒟 : DisplacementAlgebra (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) - 𝒟 = Endo H Δ⁺ + 𝒟 : Displacement-algebra (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) + 𝒟 = Endo∘ H Δ⁺ SOrdᴴ : Precategory (o ⊔ r ⊔ (lsuc o ⊔ lsuc r)) (o ⊔ r ⊔ (lsuc o ⊔ lsuc r)) SOrdᴴ = Eilenberg-Moore _ H @@ -53,22 +57,24 @@ module _ {o r} (H : HierarchyTheory o r) (Δ : StrictOrder o r) (Ψ : Set (lsuc SOrdᴹᴰ : Precategory _ _ SOrdᴹᴰ = Eilenberg-Moore _ (ℳ 𝒟) - Fᴴ⟨_⟩ : StrictOrder o r → Algebra (StrictOrders o r) H - Fᴴ⟨_⟩ = Functor.F₀ (Free (StrictOrders o r) H) + Fᴴ⟨_⟩ : Strict-order o r → Algebra (Strict-orders o r) H + Fᴴ⟨_⟩ = Functor.F₀ (Free (Strict-orders o r) H) - Fᴹᴰ⟨_⟩ : StrictOrder (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra (StrictOrders (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r)) (ℳ 𝒟) - Fᴹᴰ⟨_⟩ = Functor.F₀ (Free (StrictOrders (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r)) (ℳ 𝒟)) + Fᴹᴰ⟨_⟩ : Strict-order (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra (Strict-orders (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r)) (ℳ 𝒟) + Fᴹᴰ⟨_⟩ = Functor.F₀ (Free (Strict-orders (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r)) (ℳ 𝒟)) - module Δ = StrictOrder Δ + module Δ = Strict-order Δ - module 𝒟 = DisplacementAlgebra 𝒟 + module 𝒟 = Displacement-algebra 𝒟 module H = Monad H module HR = FR H.M module ℳᴰ = Monad (ℳ 𝒟) - module H⟨Δ⁺⟩ = StrictOrder (H.M₀ Δ⁺) - module Fᴹᴰ⟨Δ⁺⟩ = StrictOrder (fst (Fᴹᴰ⟨ Lift< (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) Δ⁺ ⟩)) - module Fᴹᴰ⟨Ψ⟩ = StrictOrder (fst (Fᴹᴰ⟨ Disc Ψ ⟩)) - module SOrd {o} {r} = Cat (StrictOrders o r) + module H⟨Δ⁺⟩ = Strict-order (H.M₀ Δ⁺) + module H⟨Δ⟩ = Strict-order (H.M₀ Δ) + module Fᴹᴰ⟨Δ⁺⟩ = Strict-order (fst (Fᴹᴰ⟨ Lift< (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) Δ⁺ ⟩)) + module Fᴹᴰ⟨Ψ⟩ = Strict-order (fst (Fᴹᴰ⟨ Disc Ψ ⟩)) + module H⟨Δ⁺⟩→ = Displacement-algebra (Endo∘ H Δ⁺) + module SOrd {o} {r} = Cat (Strict-orders o r) module SOrdᴴ = Cat (SOrdᴴ) module SOrdᴹᴰ = Cat (SOrdᴹᴰ) @@ -77,94 +83,95 @@ module _ {o r} (H : HierarchyTheory o r) (Δ : StrictOrder o r) (Ψ : Set (lsuc pattern ι₁ α = inr (inl α) pattern ι₂ α = inr (inr α) - ι₁-hom : Precategory.Hom (StrictOrders o r) Δ Δ⁺ - ι₁-hom ._⟨$⟩_ = ι₁ - ι₁-hom .homo α<β = α<β + ι₁-hom : Precategory.Hom (Strict-orders o r) Δ Δ⁺ + ι₁-hom .hom = ι₁ + ι₁-hom .strict-mono α<β = α<β ι₁-monic : SOrd.is-monic ι₁-hom - ι₁-monic g h p = strict-order-path λ α → - inl-inj (inr-inj (strict-order-happly p α )) + ι₁-monic g h p = ext λ α → + inl-inj (inr-inj (p #ₚ α)) + -------------------------------------------------------------------------------- -- Construction of the functor T -- Section 3.4, Lemma 3.8 - module _ (σ : Algebra-hom _ H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) where - open Cat (StrictOrders o r) - - σ̅ : Hom Δ⁺ (H.M₀ Δ⁺) - σ̅ ⟨$⟩ ι₀ α = H.unit.η _ ⟨$⟩ ι₀ α - σ̅ ⟨$⟩ ι₁ α = H.M₁ ι₁-hom ⟨$⟩ σ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - σ̅ ⟨$⟩ ι₂ α = H.unit.η _ ⟨$⟩ ι₂ α - σ̅ .homo {ι₀ ⋆} {ι₀ ⋆} (lift ff) = absurd ff - σ̅ .homo {ι₁ α} {ι₁ β} α<β = (H.M₁ ι₁-hom SOrd.∘ σ .morphism SOrd.∘ H.unit.η Δ) .homo α<β - σ̅ .homo {ι₂ α} {ι₂ β} α<β = H.unit.η Δ⁺ .homo α<β - - T′ : Algebra-hom _ H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩ - T′ .morphism = H.mult.η _ ∘ H.M₁ σ̅ - T′ .commutes = strict-order-path λ α → - H.mult.η _ ⟨$⟩ H.M₁ σ̅ ⟨$⟩ H.mult.η _ ⟨$⟩ α ≡˘⟨ ap (H.mult.η _ ⟨$⟩_) (strict-order-happly (H.mult.is-natural _ _ σ̅) α) ⟩ - H.mult.η _ ⟨$⟩ H.mult.η _ ⟨$⟩ H.M₁ (H.M₁ σ̅) ⟨$⟩ α ≡˘⟨ strict-order-happly H.mult-assoc (H.M₁ (H.M₁ σ̅) ⟨$⟩ α) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (H.mult.η _) ⟨$⟩ H.M₁ (H.M₁ σ̅) ⟨$⟩ α ≡˘⟨ ap (H.mult.η _ ⟨$⟩_) (strict-order-happly (H.M-∘ (H.mult.η _) (H.M₁ σ̅)) α) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (H.mult.η _ ∘ H.M₁ σ̅) ⟨$⟩ α ∎ + σ̅ : (σ : Algebra-hom _ H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → Hom Δ⁺ (H.M₀ Δ⁺) + σ̅ σ .hom (ι₀ α) = H.unit.η _ # ι₀ α + σ̅ σ .hom (ι₁ α) = H.M₁ ι₁-hom # (σ # (H.unit.η _ # α)) + σ̅ σ .hom (ι₂ α) = H.unit.η _ # ι₂ α + σ̅ σ .strict-mono {ι₀ ⋆} {ι₀ ⋆} (lift ff) = absurd ff + σ̅ σ .strict-mono {ι₁ α} {ι₁ β} α<β = (H.M₁ ι₁-hom SOrd.∘ σ .morphism SOrd.∘ H.unit.η Δ) .strict-mono α<β + σ̅ σ .strict-mono {ι₂ α} {ι₂ β} α<β = H.unit.η Δ⁺ .strict-mono α<β + + σ̅-id : σ̅ SOrdᴴ.id ≡ H.unit.η _ + σ̅-id = ext λ where + (ι₀ α) → refl + (ι₁ α) → (sym (H.unit.is-natural _ _ ι₁-hom)) #ₚ α + (ι₂ α) → refl + + σ̅-ι + : ∀ (σ : Algebra-hom _ H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) + → (α : ⌞ H.M₀ Δ ⌟) + → H.M₁ (H.M₁ ι₁-hom) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η _) # α)) + ≡ H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) + σ̅-ι σ α = + (H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism) ∘ H.M₁ (H.unit.η _)) # α ≡˘⟨ (H.M-∘ _ _ ∙ ap (H.M₁ (H.M₁ ι₁-hom) ∘_) (H.M-∘ _ _)) #ₚ α ⟩ + H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η _) # α ≡⟨ ap (λ e → H.M₁ e # α) lemma ⟩ + H.M₁ (σ̅ σ ∘ ι₁-hom) # α ≡⟨ (H.M-∘ _ _ #ₚ α) ⟩ + H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) ∎ + where + lemma : H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η _ ≡ σ̅ σ ∘ ι₁-hom + lemma = ext λ _ → refl + + σ̅-∘ : ∀ (σ δ : Algebra-hom _ H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → σ̅ (σ SOrdᴴ.∘ δ) ≡ H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ + σ̅-∘ σ δ = ext λ where + (ι₀ α) → + 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.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.unit.η _ # ι₂ α ≡˘⟨ H.right-ident #ₚ _ ⟩ + H.mult.η _ # (H.unit.η _ # (H.unit.η _ # ι₂ α)) ≡⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (σ̅ σ) #ₚ (ι₂ α)) ⟩ + H.mult.η _ # (H.M₁ (σ̅ σ) # (H.unit.η _ # ι₂ α)) ∎ + + T′ : (σ : Algebra-hom _ H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → Algebra-hom _ H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩ + T′ σ .morphism = H.mult.η _ ∘ 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.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 - open Cat (StrictOrders o r) - - σ̅-id : σ̅ SOrdᴴ.id ≡ H.unit.η _ - σ̅-id = strict-order-path λ where - (ι₀ α) → refl - (ι₁ α) → strict-order-happly (sym (H.unit.is-natural _ _ ι₁-hom)) α - (ι₂ α) → refl - - σ̅-∘ : ∀ (σ δ : Algebra-hom _ H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → σ̅ (σ SOrdᴴ.∘ δ) ≡ H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ - σ̅-∘ σ δ = strict-order-path λ where - (ι₀ α) → - H.unit.η _ ⟨$⟩ ι₀ α ≡˘⟨ strict-order-happly H.right-ident (H.unit.η _ ⟨$⟩ ι₀ α) ⟩ - H.mult.η _ ⟨$⟩ H.unit.η _ ⟨$⟩ H.unit.η _ ⟨$⟩ ι₀ α ≡⟨ ap (H.mult.η _ ⟨$⟩_) (strict-order-happly (H.unit.is-natural _ _ (σ̅ σ)) (ι₀ α)) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (σ̅ σ) ∘ H.unit.η _ ⟨$⟩ ι₀ α ∎ - (ι₁ α) → - H.M₁ ι₁-hom ⟨$⟩ σ .morphism ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - ≡˘⟨ ap (λ ϕ → H.M₁ ι₁-hom ⟨$⟩ σ .morphism ⟨$⟩ ϕ) (strict-order-happly H.left-ident _) ⟩ - H.M₁ ι₁-hom ⟨$⟩ σ .morphism ⟨$⟩ H.mult.η _ ⟨$⟩ H.M₁ (H.unit.η _) ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - ≡⟨ ap ( H.M₁ ι₁-hom ⟨$⟩_) (strict-order-happly (σ .commutes) _) ⟩ - H.M₁ ι₁-hom ⟨$⟩ H.mult.η _ ⟨$⟩ H.M₁ (σ .morphism) ⟨$⟩ H.M₁ (H.unit.η _) ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - ≡˘⟨ strict-order-happly (H.mult.is-natural _ _ ι₁-hom) _ ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (H.M₁ ι₁-hom) ⟨$⟩ H.M₁ (σ .morphism) ⟨$⟩ H.M₁ (H.unit.η _) ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - ≡˘⟨ ap (λ ϕ → H.mult.η _ ∘ ϕ ∘ δ .morphism ∘ H.unit.η _ ⟨$⟩ α) (H.M-∘ _ _ ∙ ap (H.M₁ (H.M₁ ι₁-hom) ∘_) (H.M-∘ _ _)) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η _) ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - ≡⟨ ap (λ ϕ → H.mult.η _ ⟨$⟩ H.M₁ ϕ ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α) (strict-order-path λ _ → refl) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (σ̅ σ ∘ ι₁-hom) ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α - ≡⟨ ap (λ ϕ → H.mult.η _ ⟨$⟩ ϕ ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α) (H.M-∘ _ _) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (σ̅ σ) ⟨$⟩ H.M₁ ι₁-hom ⟨$⟩ δ .morphism ⟨$⟩ H.unit.η _ ⟨$⟩ α ∎ - (ι₂ α) → - H.unit.η _ ⟨$⟩ ι₂ α ≡˘⟨ strict-order-happly H.right-ident (H.unit.η _ ⟨$⟩ ι₂ α) ⟩ - H.mult.η _ ⟨$⟩ H.unit.η _ ⟨$⟩ H.unit.η _ ⟨$⟩ ι₂ α ≡⟨ ap (H.mult.η _ ⟨$⟩_) (strict-order-happly (H.unit.is-natural _ _ (σ̅ σ)) (ι₂ α)) ⟩ - H.mult.η _ ⟨$⟩ H.M₁ (σ̅ σ) ∘ H.unit.η _ ⟨$⟩ ι₂ α ∎ - functor : Functor (Endos SOrdᴴ Fᴴ⟨ Δ ⟩) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩) functor .Functor.F₀ _ = tt - functor .Functor.F₁ σ .morphism ⟨$⟩ (α , d) = α , (T′ σ SOrdᴴ.∘ d) - functor .Functor.F₁ σ .morphism .homo {α , d1} {β , d2} = + functor .Functor.F₁ σ .morphism .hom (α , d) = α , (T′ σ SOrdᴴ.∘ d) + functor .Functor.F₁ σ .morphism .strict-mono {α , d1} {β , d2} = ⋉-elim (λ α≡β d1 Uᴹᴰ F∘ T ν pt = nt where - open Cat (StrictOrders o r) - ℓ̅ : ⌞ H.M₀ Δ ⌟ → Hom Δ⁺ (H.M₀ Δ⁺) - ℓ̅ ℓ ⟨$⟩ ι₀ _ = H.M₁ ι₁-hom ⟨$⟩ ℓ - ℓ̅ ℓ ⟨$⟩ ι₁ α = H.unit.η _ ⟨$⟩ ι₂ α - ℓ̅ ℓ ⟨$⟩ ι₂ α = H.unit.η _ ⟨$⟩ ι₂ α - ℓ̅ ℓ .homo {ι₀ α} {ι₀ β} (lift ff) = absurd ff - ℓ̅ ℓ .homo {ι₁ α} {ι₁ β} α<β = H.unit.η _ .homo α<β - ℓ̅ ℓ .homo {ι₂ α} {ι₂ β} α<β = H.unit.η _ .homo α<β - - ℓ̅-mono : ∀ {ℓ ℓ′} → H.M₀ Δ [ ℓ′ < ℓ ] → ∀ α → H.M₀ Δ⁺ [ ℓ̅ ℓ′ ⟨$⟩ α ≤ ℓ̅ ℓ ⟨$⟩ α ] - ℓ̅-mono ℓ′<ℓ (ι₀ _) = inr (H.M₁ ι₁-hom .homo ℓ′<ℓ) + ℓ̅ ℓ .hom (ι₀ _) = H.M₁ ι₁-hom # ℓ + ℓ̅ ℓ .hom (ι₁ α) = H.unit.η _ # ι₂ α + ℓ̅ ℓ .hom (ι₂ α) = H.unit.η _ # ι₂ α + ℓ̅ ℓ .strict-mono {ι₀ α} {ι₀ β} (lift ff) = absurd ff + ℓ̅ ℓ .strict-mono {ι₁ α} {ι₁ β} α<β = H.unit.η _ .strict-mono α<β + ℓ̅ ℓ .strict-mono {ι₂ α} {ι₂ β} α<β = H.unit.η _ .strict-mono α<β + + ℓ̅-mono : ∀ {ℓ ℓ′} → ℓ′ H⟨Δ⟩.< ℓ → ∀ (α : ⌞ Δ⁺ ⌟) → ℓ̅ ℓ′ # α H⟨Δ⁺⟩.≤ ℓ̅ ℓ # α + ℓ̅-mono ℓ′<ℓ (ι₀ _) = inr (H.M₁ ι₁-hom .strict-mono ℓ′<ℓ) ℓ̅-mono ℓ′<ℓ (ι₁ _) = inl refl ℓ̅-mono ℓ′<ℓ (ι₂ _) = inl refl ν′ : ⌞ H.M₀ Δ ⌟ → Algebra-hom _ H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩ ν′ ℓ .morphism = H.mult.η _ ∘ H.M₁ (ℓ̅ ℓ) - ν′ ℓ .commutes = strict-order-path λ α → - H.mult.η _ ∘ HR.F₁ (ℓ̅ ℓ) ∘ H.mult.η _ ⟨$⟩ α ≡˘⟨ strict-order-happly (refl⟩∘⟨ (H.mult.is-natural _ _ (ℓ̅ ℓ))) α ⟩ - H.mult.η _ ∘ H.mult.η _ ∘ H.M₁ (H.M₁ (ℓ̅ ℓ)) ⟨$⟩ α ≡⟨ strict-order-happly (extendl (sym H.mult-assoc)) α ⟩ - H.mult.η _ ∘ HR.F₁ (H.mult.η _) ∘ H.M₁ (H.M₁ (ℓ̅ ℓ)) ⟨$⟩ α ≡˘⟨ strict-order-happly (refl⟩∘⟨ H.M-∘ _ _) α ⟩ - H.mult.η _ ∘ HR.F₁ (H.mult.η _ ∘ 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.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₁ (ℓ̅ ℓ)) # α) ∎ - ν′-strictly-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → H.M₀ Δ [ ℓ′ < ℓ ] → Endo H Δ⁺ [ ν′ ℓ′ < ν′ ℓ ]ᵈ + ν′-strictly-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.< ℓ → ν′ ℓ′ H⟨Δ⁺⟩→.< ν′ ℓ ν′-strictly-mono {ℓ′} {ℓ} ℓ′<ℓ .endo[_<_].endo-≤ α = begin-≤ - H.mult.η _ ∘ HR.F₁ (ℓ̅ ℓ′) ∘ H.unit.η _ ⟨$⟩ α ≡̇⟨ strict-order-happly (refl⟩∘⟨ (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′))) α ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ ℓ̅ ℓ′ ⟨$⟩ α ≤⟨ strictly-mono→mono (H.mult.η _ ∘ H.unit.η _) (ℓ̅-mono ℓ′<ℓ α) ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ ℓ̅ ℓ ⟨$⟩ α ≡̇⟨ strict-order-happly (refl⟩∘⟨ H.unit.is-natural _ _ (ℓ̅ ℓ)) α ⟩ - H.mult.η _ ∘ HR.F₁ (ℓ̅ ℓ) ∘ H.unit.η _ ⟨$⟩ α <∎ + H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # α)) ≡̇⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ α) ⟩ + H.mult.η _ # (H.unit.η _ # (ℓ̅ ℓ′ # α)) ≤⟨ mono (H.mult.η _ ∘ H.unit.η _) (ℓ̅-mono ℓ′<ℓ α) ⟩ + H.mult.η _ # (H.unit.η _ # (ℓ̅ ℓ # α)) ≡̇⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ + H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # α)) <∎ where - open StrictOrder-Reasoning (H.M₀ Δ⁺) + open Mugen.Order.StrictOrder.Reasoning (H.M₀ Δ⁺) ν′-strictly-mono {ℓ′} {ℓ} ℓ′<ℓ .endo[_<_].endo-< = inc (ι₀ ⋆ , ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩) where - open StrictOrder-Reasoning (H.M₀ Δ⁺) + open Mugen.Order.StrictOrder.Reasoning (H.M₀ Δ⁺) - ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ : H.M₀ Δ⁺ [ H.mult.η _ ∘ H.M₁ (ℓ̅ ℓ′) ∘ H.unit.η _ ⟨$⟩ ι₀ ⋆ < H.mult.η _ ∘ H.M₁ (ℓ̅ ℓ) ∘ H.unit.η _ ⟨$⟩ ι₀ ⋆ ] + ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ : H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # (ι₀ ⋆))) H⟨Δ⁺⟩.< H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # (ι₀ ⋆))) ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ = begin-< - H.mult.η _ ∘ HR.F₁ (ℓ̅ ℓ′) ∘ H.unit.η _ ⟨$⟩ ι₀ ⋆ ≡̇⟨ strict-order-happly (refl⟩∘⟨ (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′))) (ι₀ ⋆) ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom ⟨$⟩ ℓ′ <⟨ (H.mult.η _ ∘ (H.unit.η _ ∘ H.M₁ ι₁-hom)) .homo ℓ′<ℓ ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom ⟨$⟩ ℓ ≡̇⟨ strict-order-happly (refl⟩∘⟨ (H.unit.is-natural _ _ (ℓ̅ ℓ))) (ι₀ ⋆) ⟩ - H.mult.η _ ∘ H.M₁ (ℓ̅ ℓ) ∘ H.unit.η _ ⟨$⟩ ι₀ ⋆ <∎ + H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # ι₀ ⋆)) ≡̇⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ _) ⟩ + H.mult.η _ # (H.unit.η _ # (H.M₁ ι₁-hom # ℓ′)) <⟨ (H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom) .strict-mono ℓ′<ℓ ⟩ + H.mult.η _ # (H.unit.η _ # (H.M₁ ι₁-hom # ℓ)) ≡̇⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ _) ⟩ + H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # ι₀ ⋆)) <∎ - ℓ̅-σ̅ : ∀ {ℓ : ⌞ fst Fᴴ⟨ Δ ⟩ ⌟} (σ : Algebra-hom _ _ Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → ℓ̅ (σ .morphism ⟨$⟩ ℓ) ≡ H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ - ℓ̅-σ̅ {ℓ} σ = strict-order-path λ where + ℓ̅-σ̅ : ∀ {ℓ : ⌞ fst Fᴴ⟨ Δ ⟩ ⌟} (σ : Algebra-hom _ _ Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → ℓ̅ (σ # ℓ) ≡ H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ + ℓ̅-σ̅ {ℓ} σ = ext λ where (ι₀ ⋆) → - H.M₁ ι₁-hom ∘ σ .morphism ⟨$⟩ ℓ ≡⟨ strict-order-happly (refl⟩∘⟨ (intror H.left-ident)) ℓ ⟩ - H.M₁ ι₁-hom ∘ σ .morphism ∘ H.mult.η _ ∘ H.M₁ (H.unit.η _) ⟨$⟩ ℓ ≡⟨ strict-order-happly (refl⟩∘⟨ pulll (σ .commutes)) ℓ ⟩ - H.M₁ ι₁-hom ∘ H.mult.η _ ∘ H.M₁ (σ .morphism) ∘ H.M₁ (H.unit.η _) ⟨$⟩ ℓ ≡⟨ strict-order-happly (pulll (sym $ H.mult.is-natural _ _ ι₁-hom)) ℓ ⟩ - H.mult.η _ ∘ H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism) ∘ H.M₁ (H.unit.η _) ⟨$⟩ ℓ ≡⟨ strict-order-happly (refl⟩∘⟨ refl⟩∘⟨ (sym $ H.M-∘ _ _)) ℓ ⟩ - H.mult.η _ ∘ H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism ∘ H.unit.η _) ⟨$⟩ ℓ ≡⟨ strict-order-happly (refl⟩∘⟨ (sym $ H.M-∘ _ _)) ℓ ⟩ - H.mult.η _ ∘ H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η _) ⟨$⟩ ℓ ≡⟨ strict-order-happly (refl⟩∘⟨ (H.M-∘ (σ̅ σ) ι₁-hom)) ℓ ⟩ - H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ H.M₁ ι₁-hom ⟨$⟩ ℓ ∎ + 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.unit.η _ ⟨$⟩ ι₂ α ≡⟨ strict-order-happly {f = H.unit.η _} (introl H.right-ident) (ι₂ α) ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ H.unit.η _ ⟨$⟩ ι₂ α ≡⟨ strict-order-happly (refl⟩∘⟨ H.unit.is-natural _ _ (σ̅ σ)) (ι₂ α) ⟩ - H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ H.unit.η _ ⟨$⟩ ι₂ α ∎ + 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.unit.η _ ⟨$⟩ ι₂ α ≡⟨ strict-order-happly {f = H.unit.η _} (introl H.right-ident) (ι₂ α) ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ H.unit.η _ ⟨$⟩ ι₂ α ≡⟨ strict-order-happly (refl⟩∘⟨ H.unit.is-natural _ _ (σ̅ σ)) (ι₂ α) ⟩ - H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ H.unit.η _ ⟨$⟩ ι₂ α ∎ + H.unit.η _ # ι₂ α ≡˘⟨ H.right-ident #ₚ _ ⟩ + H.mult.η _ # (H.unit.η _ # (H.unit.η _ # ι₂ α)) ≡⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (σ̅ σ) #ₚ (ι₂ α)) ⟩ + H.mult.η _ # (H.M₁ (σ̅ σ) # (H.unit.η _ # ι₂ α)) ∎ nt : Uᴴ => Uᴹᴰ F∘ T - nt ._=>_.η _ ⟨$⟩ (lift ℓ) = pt , ν′ ℓ - nt ._=>_.η _ .homo (lift ℓ<ℓ′) = biased refl (ν′-strictly-mono ℓ<ℓ′) - nt ._=>_.is-natural _ _ σ = strict-order-path λ ℓ → - Σ-pathp refl $ Algebra-hom-path _ $ strict-order-path λ α → - H.mult.η _ ∘ H.M₁ (ℓ̅ (σ .morphism ⟨$⟩ ℓ .Lift.lower)) ⟨$⟩ α ≡⟨ ap (λ ϕ → (H.mult.η _ ∘ H.M₁ ϕ) ⟨$⟩ α) (ℓ̅-σ̅ σ) ⟩ - H.mult.η _ ∘ H.M₁ (H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ (ℓ .Lift.lower)) ⟨$⟩ α ≡⟨ strict-order-happly (refl⟩∘⟨ H.M-∘ _ _) α ⟩ - H.mult.η _ ∘ H.M₁ (H.mult.η _) ∘ H.M₁ (H.M₁ (σ̅ σ) ∘ ℓ̅ (ℓ .Lift.lower)) ⟨$⟩ α ≡⟨ strict-order-happly (refl⟩∘⟨ refl⟩∘⟨ H.M-∘ _ _) α ⟩ - H.mult.η _ ∘ H.M₁ (H.mult.η _) ∘ H.M₁ (H.M₁ (σ̅ σ)) ∘ H.M₁ (ℓ̅ (ℓ .Lift.lower)) ⟨$⟩ α ≡⟨ strict-order-happly (pulll H.mult-assoc) α ⟩ - H.mult.η _ ∘ H.mult.η _ ∘ H.M₁ (H.M₁ (σ̅ σ)) ∘ H.M₁ (ℓ̅ (ℓ .Lift.lower)) ⟨$⟩ α ≡⟨ strict-order-happly (refl⟩∘⟨ pulll (H.mult.is-natural _ _ (σ̅ σ))) α ⟩ - H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ H.mult.η _ ∘ H.M₁ (ℓ̅ (ℓ .Lift.lower)) ⟨$⟩ α ∎ + nt ._=>_.η _ .hom (lift ℓ) = pt , ν′ ℓ + nt ._=>_.η _ .strict-mono (lift ℓ<ℓ′) = biased refl (ν′-strictly-mono ℓ<ℓ′) + nt ._=>_.is-natural _ _ σ = ext λ ℓ → + refl , λ α → + H.mult.η _ # (H.M₁ (ℓ̅ (σ # ℓ .Lift.lower)) # α) ≡⟨ ap (λ e → (H.mult.η _ ∘ H.M₁ e) # α) (ℓ̅-σ̅ σ) ⟩ + H.mult.η _ # (H.M₁ (H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ (ℓ .Lift.lower)) # α) ≡⟨ ap (H.mult.η _ #_) ((H.M-∘ _ _ ∙ ((refl⟩∘⟨ H.M-∘ _ _))) #ₚ α) ⟩ + H.mult.η _ # (H.M₁ (H.mult.η _) # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (ℓ̅ (ℓ .Lift.lower)) # α))) ≡⟨ H.mult-assoc #ₚ _ ⟩ + H.mult.η _ # (H.mult.η _ # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (ℓ̅ (ℓ .Lift.lower)) # α))) ≡⟨ ap (H.mult.η _ #_) (H.mult.is-natural _ _ (σ̅ σ) #ₚ _) ⟩ + H.mult.η _ # (H.M₁ (σ̅ σ) # (H.mult.η _ # (H.M₁ (ℓ̅ (ℓ .Lift.lower)) # α))) ∎ -------------------------------------------------------------------------------- -- Faithfulness of T @@ -275,19 +275,10 @@ module _ {o r} (H : HierarchyTheory o r) (Δ : StrictOrder o r) (Ψ : Set (lsuc T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T T-faithful pt H-preserves-monos {x} {y} {σ} {δ} p = free-algebra-path $ H-preserves-monos ι₁-hom ι₁-monic _ _ $ - strict-order-path λ α → - -- NOTE: More pointless reasoning steps because of unifier failures!! - H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η _ ⟨$⟩ α ≡⟨⟩ - σ̅ σ ⟨$⟩ (ι₁ α) ≡⟨ strict-order-happly (introl H.right-ident {f = σ̅ σ}) (ι₁ α) ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ σ̅ σ ⟨$⟩ (ι₁ α) ≡⟨ strict-order-happly (assoc (H.mult.η _) (H.unit.η _) (σ̅ σ)) (ι₁ α) ⟩ - H.mult.η _ ∘ (H.unit.η _ ∘ σ̅ σ) ⟨$⟩ (ι₁ α) ≡⟨ ap (λ ϕ → H.mult.η _ ∘ ϕ ⟨$⟩ (ι₁ α)) (H.unit.is-natural _ _ (σ̅ σ)) ⟩ - H.mult.η _ ∘ (H.M₁ (σ̅ σ) ∘ H.unit.η _) ⟨$⟩ (ι₁ α) ≡˘⟨ strict-order-happly (assoc (H.mult.η _) (H.M₁ (σ̅ σ)) (H.unit.η _)) (ι₁ α) ⟩ - H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ H.unit.η _ ⟨$⟩ (ι₁ α) ≡⟨ hierarchy-algebra-happly (ap snd $ hierarchy-algebra-happly p (pt , SOrdᴴ.id)) (H.unit.η _ ⟨$⟩ ι₁ α) ⟩ - H.mult.η _ ∘ H.M₁ (σ̅ δ) ∘ H.unit.η _ ⟨$⟩ (ι₁ α) ≡˘⟨ strict-order-happly (assoc (H.mult.η _) (H.M₁ (σ̅ δ)) (H.unit.η _)) (ι₁ α) ⟩ - H.mult.η _ ∘ (H.M₁ (σ̅ δ) ∘ H.unit.η _) ⟨$⟩ (ι₁ α) ≡˘⟨ ap (λ ϕ → H.mult.η _ ∘ ϕ ⟨$⟩ (ι₁ α)) (H.unit.is-natural _ _ (σ̅ δ)) ⟩ - H.mult.η _ ∘ (H.unit.η _ ∘ σ̅ δ) ⟨$⟩ (ι₁ α) ≡˘⟨ strict-order-happly (assoc (H.mult.η _) (H.unit.η _) (σ̅ δ)) (ι₁ α) ⟩ - H.mult.η _ ∘ H.unit.η _ ∘ σ̅ δ ⟨$⟩ (ι₁ α) ≡⟨ strict-order-happly (eliml H.right-ident {f = σ̅ δ}) (ι₁ α) ⟩ - σ̅ δ ⟨$⟩ (ι₁ α) ≡⟨⟩ - H.M₁ ι₁-hom ∘ δ .morphism ∘ H.unit.η _ ⟨$⟩ α ∎ - where - open Cat (StrictOrders o r) + 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 #ₚ _ ⟩ + σ̅ δ # (ι₁ α) ∎ diff --git a/src/Mugen/Cat/StrictOrders.agda b/src/Mugen/Cat/StrictOrders.agda index 967c429..c9a7a90 100644 --- a/src/Mugen/Cat/StrictOrders.agda +++ b/src/Mugen/Cat/StrictOrders.agda @@ -5,45 +5,34 @@ open import Mugen.Order.StrictOrder private variable o r : Level - X Y Z : StrictOrder o r + X Y Z : Strict-order o r -------------------------------------------------------------------------------- -- The Category of Strict Orders open Precategory -open StrictOrder-on -open is-strict-order -strict-order-id : StrictOrder-Hom X X -strict-order-id {X = X} = homomorphism (λ x → x) (λ xy y>z = trans y>z x>y - - op-is-strict-order : is-strict-order (op A [_<_]) - op-is-strict-order .is-strict-order.irrefl {x} = op-irrefl x - op-is-strict-order .is-strict-order.trans {x} {y} {z} = op-trans x y z - op-is-strict-order .is-strict-order.has-prop = has-prop + from-op≤ : ∀ {x y} → x op≤ y → non-strict _op<_ x y + from-op≤ (inl y≡x) = inl (sym y≡x) + from-op≤ (inr y