Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@favonia
favonia committed Jun 4, 2024
1 parent 2c1ee05 commit bf4f486
Show file tree
Hide file tree
Showing 3 changed files with 134 additions and 114 deletions.
226 changes: 112 additions & 114 deletions src/Mugen/Cat/HierarchyTheory.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,127 +22,125 @@ Hierarchy-theory o r = Monad (Strict-orders o r)
--------------------------------------------------------------------------------
-- Morphisms between hierarchy theories

private
M∘-functor : ∀ {o r} →
Functor
(Cat[ Strict-orders o r , Strict-orders o r ] ×ᶜ Cat[ Strict-orders o r , Strict-orders o r ])
Cat[ Strict-orders o r , Strict-orders o r ]
M∘-functor = F∘-functor

module M∘ {o r : Level} = Functor (M∘-functor {o} {r})

record Hierarchy-map {o r} (M N : Hierarchy-theory o r) : Type (lsuc o ⊔ lsuc r) where
no-eta-equality
module M = Monad M
module N = Monad N
field
nat : M.M => N.M
open _=>_ nat public
field
pres-unit : nat ∘nt M.unit ≡ N.unit
pres-mult : nat ∘nt M.mult ≡ N.mult ∘nt (nat ◆ nat)

module _ {o r} {M N : Hierarchy-theory o r} (ν1 ν2 : Hierarchy-map M N) where
module _ {o r} where
private
module M = Monad M
module N = Monad N
SOrd : Precategory (lsuc (o ⊔ r)) (o ⊔ r)
SOrd = Strict-orders o r

Hierarchy-map-path
: ν1 .Hierarchy-map.nat ≡ ν2 .Hierarchy-map.nat
→ ν1 ≡ ν2
Hierarchy-map-path p i .Hierarchy-map.nat = p i
Hierarchy-map-path p i .Hierarchy-map.pres-unit =
is-prop→pathp
(λ i → Nat-is-set (p i ∘nt M.unit) N.unit)
(ν1 .Hierarchy-map.pres-unit)
(ν2 .Hierarchy-map.pres-unit)
i
Hierarchy-map-path p i .Hierarchy-map.pres-mult =
is-prop→pathp
(λ i → Nat-is-set (p i ∘nt M.mult) (N.mult ∘nt (p i ◆ p i)))
(ν1 .Hierarchy-map.pres-mult)
(ν2 .Hierarchy-map.pres-mult)
i

module _ {o r} {M N : Hierarchy-theory o r} where
private
module M = Monad M
module N = Monad N
Endo : Precategory (lsuc (o ⊔ r)) (lsuc (o ⊔ r))
Endo = Cat[ SOrd , SOrd ]
module Endo = Cat Endo

abstract instance
H-Level-Hierarchy-map : ∀ {n} → H-Level (Hierarchy-map M N) (2 + n)
H-Level-Hierarchy-map = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)
where unquoteDecl eqv = declare-record-iso eqv (quote Hierarchy-map)

instance
Extensional-Hierarchy-map
: ∀ {ℓ} ⦃ sa : Extensional (M.M => N.M) ℓ ⦄
→ Extensional (Hierarchy-map M N) ℓ
Extensional-Hierarchy-map ⦃ sa ⦄ =
injection→extensional!
{f = Hierarchy-map.nat}
(Hierarchy-map-path _ _) sa

Funlike-Hierarchy-map
: Funlike (Hierarchy-map M N) (Poset o r) (λ Δ → Strictly-monotone (M.M # Δ) (N.M # Δ))
Funlike-Hierarchy-map ._#_ = Hierarchy-map.η

Hierarchy-map-id : ∀ {o r} {M : Hierarchy-theory o r} → Hierarchy-map M M
Hierarchy-map-id {M = M} = hm where
module M = Monad M

abstract
pres-unit : idnt ∘nt M.unit ≡ M.unit
pres-unit = ext λ Δ α → refl

pres-mult : idnt ∘nt M.mult ≡ M.mult ∘nt (idnt ◆ idnt)
pres-mult = ext λ Δ α →
M.μ Δ # α
≡˘⟨ ap# (M.μ Δ) $ (M∘.F-id #ₚ Δ) #ₚ α ⟩
M.μ Δ # (((idnt ◆ idnt) # Δ) # α)
∎
Endo-∘-functor : Functor (Endo ×ᶜ Endo) Endo
Endo-∘-functor = F∘-functor
module Endo-∘ = Functor Endo-∘-functor

hm : Hierarchy-map M M
hm .Hierarchy-map.nat = idnt
hm .Hierarchy-map.pres-unit = pres-unit
hm .Hierarchy-map.pres-mult = pres-mult

{-
Hierarchy-map-∘ : ∀ {o r} {M N O : Hierarchy-theory o r}
→ Hierarchy-map N O
→ Hierarchy-map M N
→ Hierarchy-map M O
Hierarchy-map-∘ {M = M} {N} {O} ν ξ = hm where
module M = Monad M
module N = Monad N
module O = Monad O
module ν = Hierarchy-map ν
module ξ = Hierarchy-map ξ
nat : M.M => O.M
nat = ν.nat ∘nt ξ.nat
pres-unit : nat ∘nt M.unit ≡ O.unit
pres-unit = ext λ Δ α →
ν.η Δ # (ξ.η Δ # (M.η Δ # α))
≡⟨ ap# (ν.η Δ) $ (ξ.pres-unit #ₚ Δ) #ₚ α ⟩
ν.η Δ # (N.η Δ # α)
≡⟨ (ν.pres-unit #ₚ Δ) #ₚ α ⟩
O.η Δ # α
∎
-- The following code assumes this judgmental equality
_ : ∀ {M M' N N' : Functor SOrd SOrd} {α : M => M'} {β : N => N'} → Endo-∘.₁ (α , β) ≡ α ◆ β
_ = refl

pres-mult : nat ∘nt M.mult ≡ O.mult ∘nt (nat ◆ nat)
pres-mult = ext λ Δ α →
ν.η Δ # (ξ.η Δ # (M.μ Δ # α))
≡⟨ ? ⟩
O.μ Δ # ((nat ◆ nat) # Δ # α)
record Hierarchy-hom (M N : Hierarchy-theory o r) : Type (lsuc o ⊔ lsuc r) where
no-eta-equality
module M = Monad M
module N = Monad N
field
nat : M.M => N.M
open _=>_ nat public
field
pres-unit : nat ∘nt M.unit ≡ N.unit
pres-mult : nat ∘nt M.mult ≡ N.mult ∘nt (nat ◆ nat)

module _ {M N : Hierarchy-theory o r} where
private
module M = Monad M
module N = Monad N

Hierarchy-hom-path : (ν ξ : Hierarchy-hom M N)
→ ν .Hierarchy-hom.nat ≡ ξ .Hierarchy-hom.nat
→ ν ≡ ξ
Hierarchy-hom-path ν ξ p i .Hierarchy-hom.nat = p i
Hierarchy-hom-path ν ξ p i .Hierarchy-hom.pres-unit =
is-prop→pathp
(λ i → Nat-is-set (p i ∘nt M.unit) N.unit)
(ν .Hierarchy-hom.pres-unit)
(ξ .Hierarchy-hom.pres-unit)
i
Hierarchy-hom-path ν ξ p i .Hierarchy-hom.pres-mult =
is-prop→pathp
(λ i → Nat-is-set (p i ∘nt M.mult) (N.mult ∘nt (p i ◆ p i)))
(ν .Hierarchy-hom.pres-mult)
(ξ .Hierarchy-hom.pres-mult)
i

abstract instance
H-Level-Hierarchy-hom : ∀ {n} → H-Level (Hierarchy-hom M N) (2 + n)
H-Level-Hierarchy-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)
where unquoteDecl eqv = declare-record-iso eqv (quote Hierarchy-hom)

instance
Extensional-Hierarchy-hom
: ∀ {ℓ} ⦃ sa : Extensional (M.M => N.M) ℓ ⦄
→ Extensional (Hierarchy-hom M N) ℓ
Extensional-Hierarchy-hom ⦃ sa ⦄ =
injection→extensional!
{f = Hierarchy-hom.nat}
(Hierarchy-hom-path _ _) sa

Funlike-Hierarchy-hom
: Funlike (Hierarchy-hom M N) (Poset o r) (λ Δ → Strictly-monotone (M.M # Δ) (N.M # Δ))
Funlike-Hierarchy-hom ._#_ = Hierarchy-hom.η

hierarchy-hom-id : ∀ {M : Hierarchy-theory o r} → Hierarchy-hom M M
hierarchy-hom-id {M = _} .Hierarchy-hom.nat = idnt
hierarchy-hom-id {M = _} .Hierarchy-hom.pres-unit = Endo.idl _
hierarchy-hom-id {M = M} .Hierarchy-hom.pres-mult =
let module M = Monad M in
idnt ∘nt M.mult
≡⟨ Endo.idl _ ⟩
M.mult
≡˘⟨ Endo.idr _ ⟩
M.mult ∘nt idnt
≡˘⟨ ap (M.mult ∘nt_) Endo-∘.F-id ⟩
M.mult ∘nt (idnt ◆ idnt)
∎

hm : Hierarchy-map M O
hm .Hierarchy-map.nat = nat
hm .Hierarchy-map.pres-unit = pres-unit
hm .Hierarchy-map.pres-mult = pres-mult
-}
hierarchy-hom-∘ : ∀ {M N O : Hierarchy-theory o r}
→ Hierarchy-hom N O
→ Hierarchy-hom M N
→ Hierarchy-hom M O
hierarchy-hom-∘ {M = M} {N} {O} ν ξ = hm where
module M = Monad M
module N = Monad N
module O = Monad O
module ν = Hierarchy-hom ν
module ξ = Hierarchy-hom ξ

hm : Hierarchy-hom M O
hm .Hierarchy-hom.nat = ν.nat ∘nt ξ.nat
hm .Hierarchy-hom.pres-unit =
(ν.nat ∘nt ξ.nat) ∘nt M.unit
≡˘⟨ Endo.assoc ν.nat ξ.nat M.unit ⟩
ν.nat ∘nt (ξ.nat ∘nt M.unit)
≡⟨ ap (ν.nat ∘nt_) ξ.pres-unit ⟩
ν.nat ∘nt N.unit
≡⟨ ν.pres-unit ⟩
O.unit
∎
hm .Hierarchy-hom.pres-mult =
(ν.nat ∘nt ξ.nat) ∘nt M.mult
≡˘⟨ Endo.assoc ν.nat ξ.nat M.mult ⟩
ν.nat ∘nt (ξ.nat ∘nt M.mult)
≡⟨ ap (ν.nat ∘nt_) ξ.pres-mult ⟩
ν.nat ∘nt (N.mult ∘nt (ξ.nat ◆ ξ.nat))
≡⟨ Endo.assoc ν.nat N.mult (ξ.nat ◆ ξ.nat) ⟩
(ν.nat ∘nt N.mult) ∘nt (ξ.nat ◆ ξ.nat)
≡⟨ ap (_∘nt (ξ.nat ◆ ξ.nat)) ν.pres-mult ⟩
(O.mult ∘nt (ν.nat ◆ ν.nat)) ∘nt (ξ.nat ◆ ξ.nat)
≡˘⟨ Endo.assoc O.mult (ν.nat ◆ ν.nat) (ξ.nat ◆ ξ.nat) ⟩
O.mult ∘nt ((ν.nat ◆ ν.nat) ∘nt (ξ.nat ◆ ξ.nat))
≡˘⟨ ap (O.mult ∘nt_) $ Endo-∘.F-∘ (ν.nat , ν.nat) (ξ.nat , ξ.nat) ⟩
O.mult ∘nt ((ν.nat ∘nt ξ.nat) ◆ (ν.nat ∘nt ξ.nat))
∎

--------------------------------------------------------------------------------
-- Misc. Definitions
Expand Down
20 changes: 20 additions & 0 deletions src/Mugen/Cat/Instances/HierarchyTheories.agda
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
module Mugen.Cat.Instances.HierarchyTheories where

open import Mugen.Prelude
open import Mugen.Order.StrictOrder
open import Mugen.Cat.HierarchyTheory

--------------------------------------------------------------------------------
-- The Category of Hierarchy Theories

open Precategory

Hierarchy-theories : ∀ (o r : Level) → Precategory (lsuc (o ⊔ r)) (lsuc (o ⊔ r))
Hierarchy-theories o r .Ob = Hierarchy-theory o r
Hierarchy-theories o r .Hom = Hierarchy-hom
Hierarchy-theories o r .Hom-set _ _ = hlevel 2
Hierarchy-theories o r .id = hierarchy-hom-id
Hierarchy-theories o r ._∘_ = hierarchy-hom-∘
Hierarchy-theories o r .idr _ = ext λ _ _ → refl
Hierarchy-theories o r .idl _ = ext λ _ _ → refl
Hierarchy-theories o r .assoc _ _ _ = ext λ _ _ → refl
2 changes: 2 additions & 0 deletions src/Mugen/Everything.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,14 @@ import Mugen.Algebra.Displacement.Subalgebra
import Mugen.Algebra.OrderedMonoid
import Mugen.Cat.HierarchyTheory
import Mugen.Cat.HierarchyTheory.McBride
import Mugen.Cat.HierarchyTheory.McBrideFunctoriality
import Mugen.Cat.HierarchyTheory.Universality
import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding
import Mugen.Cat.Instances.Displacements
import Mugen.Cat.Instances.Endomorphisms
import Mugen.Cat.Instances.HierarchyTheories
import Mugen.Cat.Instances.Indexed
import Mugen.Cat.Instances.StrictOrders
import Mugen.Cat.Monad
Expand Down

0 comments on commit bf4f486

Please sign in to comment.