Koji Miyazato
LightNews LightNews
viercc.bsky.social
Koji Miyazato
@viercc.bsky.social
34 followers 57 following 290 posts
Twitter(X), GitHubなどにいるのと同一人物です
openpgp4fpr:B2E1DC9AF16599BD2D873A227BABC58075EC4EE6

興味: Haskell, 数学
Posts Replies Media Videos
viercc.bsky.social
中途半端な日本語化やめろぉ
November 4, 2025 at 4:40 AM
viercc.bsky.social
唐突に日本語が思いつけなくなって "Yay! That's exactly what I've intended." を直訳した
(screenshot of AI chat service, user's input) やった！それは私が意図した通りです。 より読みやすかったり、整理された証明とするために、 * そもそも証明の流れとして整理すべき箇所 * Agdaで記述された証明としてidiomaticでない箇所 を探していただけますか？
July 5, 2025 at 5:32 AM
viercc.bsky.social
eq : あるequivalence relation x ~ y
subst eq : eq を 関数にtransferしたもの P x -> P y
subst-subst-symなど : subst の性質を≡で表したもの
これ : subst-subst-symなどから組み立てた証明がreflに等しいこと
Agda-mode output showing "unsolved metas" Agda v2.7.0.1 _355 : ≡.trans (≡.sym (subst-subst-sym eq)) (≡.cong (subst eq) (subst-sym-subst eq)) ≡ ≡.refl
May 30, 2025 at 9:19 AM
viercc.bsky.social
なーんか筋の悪いことをしている気がする・・・
eqPD : ≡.subst (D₁ F.∘′ v″) (C.subst-subst eq₁C) (D.subst step₂ (D.subst step₁ pd)) ≡ D.subst (eqV pc) pd eqPD = begin ≡.subst (D₁ F.∘′ v″) (C.subst-subst eq₁C) (D.subst step₂ (D.subst step₁ pd)) ≡⟨ ≡.subst-∘ (C.subst-subst eq₁C) ⟩ ≡.subst D₁ (≡.cong v″ (C.subst-subst eq₁C)) (D.subst step₂ (D.subst step₁ pd)) ≡⟨ props.subst-reflexive D* _ ⟩ D.subst step₃ (D.subst step₂ (D.subst step₁ pd)) -- Proofs written using ≈-syntax have extraneous `refl` at -- the end (to guide type inference) ≡⟨ D.subst-refl ⟩ D.subst D.refl (D.subst step₃ (D.subst step₂ (D.subst step₁ pd))) ≡⟨ D.subst-subst step₃ ⟩ D.subst (D.trans step₃ D.refl) (D.subst step₂ (D.subst step₁ pd)) ≡⟨ D.subst-subst step₂ ⟩ D.subst (D.trans step₂ (D.trans step₃ D.refl)) (D.subst step₁ pd) ≡⟨ D.subst-subst step₁ ⟩ D.subst (D.trans step₁ (D.trans step₂ (D.trans step₃ D.refl))) pd ≡⟨⟩ D.subst (eqV pc) pd ∎ where open ≡.≡-Reasoning
May 29, 2025 at 8:34 AM
viercc.bsky.social
May 28, 2025 at 1:37 PM
viercc.bsky.social
painful [Note]
-- TODO: to-Uustalu-law -- -- [Note] we can't simply have to-Uustalu-law -- -- ∀ {...} (isMonad : MM.IsMonad _ _) → IsMonad _ _ -- -- because of "congruent" laws (•-cong, ...). -- -- They can't be represented in terms of `Comp`, -- because these congruences corresponds to -- hypothetical `Setoid`-based `Container`, -- and `join : Comp C C ⇒ C` being well-defined morphism -- between `Setoid`-based `Container`.
May 26, 2025 at 1:49 PM
viercc.bsky.social
自分の環境だと表示はこう(Noto Sans Mono CJK JP, 16pt)
Screenshot showing how three "dot symbols" shows on my editor. | \cdot ····· | \. ∙∙∙∙∙ | \bullet ••••• surrounded by line repeated vertical bar character (||||||...)
May 18, 2025 at 6:04 AM
viercc.bsky.social
-- Which equality (_≈_) should be used between two `Day F G X` values `(u, v)`? -- -- > u = day A B op fa gb -- > v = day A' B' op' fa' gb' -- -- Of course, equality as a dependent product can be defined: data TooStrictEq {X : Set x} : Rel (Day F G X) x' where mkStrictEq : ∀ {A : Set a} {B : Set b} → {op₁ op₂ : A × B → X} {fa₁ fa₂ : F A} {gb₁ gb₂ : G B} → op₁ ≗ op₂ → fa₁ ≈₁ fa₂ → gb₁ ≈₂ gb₂ → TooStrictEq (day A B op₁ fa₁ gb₁) (day A B op₂ fa₂ gb₂) -- But, as the name suggests, `TooStrictEq` is not what we want when defining -- Day convolution of `Functor`s. `A` and `B`, the two type parameters `Day` sums over, -- is intended to be kept abstract when consuming `Day F G X`. -- Such restriction can be represented by considering `Day F G X` as a `Setoid` -- with equivalence relation generated by the following _⊏_ relation. infix 3 _⊏_ data _⊏_ {X : Set x} : Rel (Day F G X) x' where congF : ∀ {A} {B} {op : A × B → X} {fa fa' : F A} {gb : G B} → fa ≈₁ fa' → day A B op fa gb ⊏ day A B op fa' gb congG : ∀ {A} {B} {op} {fa : F A} {gb gb' : G B} → gb ≈₂ gb' → day A B op fa gb ⊏ day A B op fa gb' link : ∀ {A A' : Set a} {B B' : Set b} (linkA : A → A') (linkB : B → B') {op : A × B → X} {op' : A' × B' → X } → (op ≗ op' ∘′ Prod.map linkA linkB) → { fa : F A } { gb : G B } → day A B op fa gb ⊏ day A' B' op' (linkA <$> fa) (linkB <$> gb)
May 17, 2025 at 12:07 PM
viercc.bsky.social
Day convolution in Agda
-- Agda source code module _ {a fa b gb : Level} (F : Set a → Set fa) (G : Set b → Set gb) where record Day {x : Level} (X : Set x) : Set (suc (a ⊔ b) ⊔ fa ⊔ gb ⊔ x) where constructor day field A : Set a B : Set b op : A × B → X comp₁ : F A comp₂ : G B mapDay : ∀ {x} {X Y : Set x} → (X → Y) → Day X → Day Y mapDay f (day A B op fa gb) = day A B (f ∘′ op) fa gb rawFunctor : ∀ {x} → RawFunctor {ℓ = x} Day rawFunctor = record { _<$>_ = mapDay }
May 17, 2025 at 12:07 PM
viercc.bsky.social
おもしろOCR
(正しくは"群の作用する可換環の上の加群")
（Googleの検索結果のスクリーンショット） タイトル:「群の作用する可換紙の上の即戦」
May 15, 2025 at 12:41 AM
viercc.bsky.social
😨
(screenshot of Agda program) record IsMonad (C : Container s p) (raw : RawMonad C) : Set (s ⊔ p) where open RawMonad raw diag : ∀ {s : S} {v : P s → S} (w : (p₁ : P s) → P (v p₁) → S) → P (s • v) → S diag {s} {v} w p = w (↖ p) (↗ p) field •-ε : ∀ (s : S) → s • F.const ε ≡ s ε-• : ∀ (s : S) → ε • F.const s ≡ s •-• : ∀ (s : S) (v : P s → S) (w : (p : P s) → P (v p) → S) → (s • v) • diag w ≡ s • (λ p → v p • w p) ↖-inner-ε : ∀ {s : S} (p : P (s • F.const ε)) → ↖ p ≡ ≡.subst P (•-ε s) p ↗-outer-ε : ∀ {s : S} (p : P (ε • F.const s)) → ↗ p ≡ ≡.subst P (ε-• s) p ↖-↖ : ∀ {s : S} {v : P s → S} {w : (p : P s) → P (v p) → S} → {p : P ((s • v) • diag w)} {q : P (s • (λ q₁ → v q₁ • w q₁))} → (p≡q : ≡.subst P (•-• s v w) p ≡ q) → ↖ (↖ p) ≡ ↖ q ↗-↖ : ∀ {s : S} {v : P s → S} {w : (p : P s) → P (v p) → S} → {p : P ((s • v) • diag w)} {q : P (s • (λ q₁ → v q₁ • w q₁))} → (p≡q : ≡.subst P (•-• s v w) p ≡ q) → (let p₁₁≡q₁ = ↖-↖ p≡q) → ≡.subst (λ r → P (v r)) p₁₁≡q₁ (↗ (↖ p)) ≡ ↖ (↗ q) ↗-↗ : ∀ {s : S} {v : P s → S} {w : (p : P s) → P (v p) → S} → {p : P ((s • v) • diag w)} {q : P (s • (λ q₁ → v q₁ • w q₁))} → (p≡q : ≡.subst P (•-• s v w) p ≡ q) → (let p₁₁≡q₁ = ↖-↖ p≡q) (let p₁₂≡q₂₁ = ↗-↖ p≡q) → ≡.dsubst₂ (λ r₁ r₂ → P (w r₁ r₂)) p₁₁≡q₁ p₁₂≡q₂₁ (↗ p) ≡ ↗ (↗ q)
May 11, 2025 at 1:47 PM
viercc.bsky.social
😁
(screenshot of Agda program) record RawMonad (C : Container s p) : Set (s ⊔ p) where open Container C renaming (Shape to S; Position to P) public infixr 7 _•_ field ε : S _•_ : (s : S) → (P s → S) → S ↖ : {s : S} → {v : P s → S} → P (s • v) → P s ↗ : {s : S} → {v : P s → S} → (p : P (s • v)) → P (v (↖ p))
May 11, 2025 at 1:47 PM
viercc.bsky.social
Implementing cs.ioc.ee/~tarmo/paper... in Agda
record RawMonad (C : Container s p) : Set (suc (s ⊔ p)) where open Container C renaming (Shape to S; Position to P) public field unit : Id ⇒ C join : Comp C C ⇒ C record RawMonad' (C : Container s p) : Set (suc (s ⊔ p)) where open Container C renaming (Shape to S; Position to P) public infixr 2 _•_ field ε : S _•_ : (s : S) → (P s → S) → S ↖ : {s : S} → {v : P s → S} → P (s • v) → P s ↗ : {s : S} → {v : P s → S} → (p : P (s • v)) → P (v (↖ p))
May 10, 2025 at 4:42 PM
viercc.bsky.social
Comonad to (monad transformer)

viercc.github.io/haddocks/coc...

Also: request for the new name for `CoT` which is temporary
Screenshot of Haddock documentation ``` -- * The @CoT@ monad transformer -- | @CoT f g@ is a @Monad@ which is based on @Monad g@ but can use @Comonad f@ -- as a context. newtype CoT f g a = CoT { runCoT :: forall r. f r -> g (a, r) } deriving stock Functor instance MFunctor (CoT f) instance Comonad f => MonadTrans (CoT f) instance (Comonad f, MonadIO g) => MonadIO (CoT f g) instance (Comonad f, Monad g) => Applicative (CoT f g) instance Functor g => Functor (CoT f g) instance (Comonad f, Monad g) => Monad (CoT f g) ```
April 9, 2025 at 1:13 AM
viercc.bsky.social
ストリング図。キャプション: "コモナドの分配法則が満たすべき等式"
March 4, 2025 at 5:20 AM
viercc.bsky.social
横着しないで\circ を挟めば大丈夫か
February 24, 2025 at 10:21 AM
viercc.bsky.social
VとWじゃなくて別の文字にしたほうがいいかも知れない
WV \to W \\ WV \to V \\ WV \to VVW \\ WV \to VWW
February 24, 2025 at 10:18 AM
viercc.bsky.social
これ
February 10, 2025 at 11:22 AM
viercc.bsky.social
Screenshot toStore :: Torsor g x => Acting g x a -> Store x a > Acting g x is isomorphic to Store x when x is g-Torsor fromStore :: Action g x => Store x a -> Acting g x a
February 3, 2025 at 12:02 PM
viercc.bsky.social
Screenshot of Haskell documentation ## Acting comonad type Acting s x = ActingT s x Identity pattern Acting :: x -> (s -> a) -> Acting s x a locate :: forall (w :: Type -> Type) s x a. Comonad w => ActingT s x w a -> x locate is Control.Comonad.Store.pos equivalent for Acting(T) direct :: forall (w :: Type -> Type) s x a. Comonad w => s -> ActingT s x w a -> a > direct is Control.Comonad.Store.peek equivalent for Acting(T) ## Acting comonad transformer newtype ActingT s x (w :: Type -> Type) a ### Constructors ActingT runActingT :: w (x, s -> a) ### Instances - ComonadHoist (ActingT s x) - Monoid s => ComonadTrans (ActingT s x) - (Monoid s, Action s x, Comonad w) => Comonad (ActingT s x w) - Functor w => Functor (ActingT s x w) -- Comonad structure of "bare" Acting x s extractA :: forall x s a. (Monoid s) => (x, s -> a) -> a extractA (_, f) = f mempty duplicateA :: forall x s a. (Semigroup s, Action s x) => (x, s -> a) -> (x, s -> (x, s -> a)) duplicateA (x, f) = (x, \s -> (s `act` x, f . (<> s))) instance (Monoid s, Action s x, Comonad w) => Comonad (ActingT s x w) where extract = extractA . extract . runActingT where duplicate = fmap ActingT . ActingT . fmap dist . duplicate . fmap duplicateA . runActingT where dist :: forall a. w (x, s -> a) -> (x, s -> w a) dist w = (x0, \s -> peek' s <$> w) where x0 = fst (extract w) peek' s (_, f) = f s
February 3, 2025 at 11:23 AM
viercc.bsky.social
Screenshot of X post by me. The content of the post is Haskell pseudocode data Act a = Act X (M -> a) instance Monoid M -- M acts X from right act :: X -> M -> X instance Comonad Act where extract (Act _ f) = f mempty duplicate (Act x f) = Act x (\m1 -> Act (x `act` m1) (\m2 -> f (m1 <> m2)) -- StreamPos ~ Act (X = M = Natural, act = (+))
February 2, 2025 at 2:23 PM
viercc.bsky.social
A distributive law of `Store Bool` over `Store Bool`!!!
-- Haskell source dist0 :: Dist Bool Bool dist0 (C a0 k) = C (f a0) $ \b -> C a0 $ \a -> h a (b `xor` f a0 `xor` f a) where f = pos . k h a b = peek (k a) b -- Haskell source data C s p x = C s (p -> x) deriving Functor instance (s ~ p) => Comonad (C s p) where extract (C s f) = f s duplicate (C s f) = C s $ \s' -> C s' f type Store s = C s s -- Haskell -- Type of distributive laws type Dist s t = forall x. Store s (Store t x) -> Store t (Store s x)
January 27, 2025 at 1:27 AM
viercc.bsky.social
リンク先のスクリーンショット: (定義)Retrofunctorの箇所
January 18, 2025 at 8:47 AM
viercc.bsky.social
Monadの合成 `Compose` はMonadにな（るとは限）らないし、Comonadも同じなんだけど、

Comonadなら`Day`という別の組み合わせかたがあるんですよね

hackage.haskell.org/package/kan-...
instance (Comonad f, Comonad g) => Comonad (Day f g) where extract (Day fb gc bca) = bca (extract fb) (extract gc) duplicate (Day fb gc bca) = Day (duplicate fb) (duplicate gc) (\fb' gc' -> Day fb' gc' bca)
January 5, 2025 at 2:57 PM
viercc.bsky.social
こういうのもある
任意の`Funtor f`に対して`Comonad (SingleLayer f)`なので、`f`として多項式でないもの、例えば`f = Cont Bool`を選べば"多項式でないComonad"ができたことになる

でも、なんというか、多項式でない部分が本質的に使われているComonadのインスタンスが思い付かないんだよなぁ
{-# LANGUAGE DeriveTraversable #-} module Comonad.SingleLayer where import Control.Comonad data SingleLayer f a = End a | Layer a (f a) deriving (Show, Eq, Functor, Foldable, Traversable) instance Functor f => Comonad (SingleLayer f) where extract (End a) = a extract (Layer a _) = a duplicate (End a) = End (End a) duplicate wa@(Layer _ fa) = Layer wa (End <$> fa)
November 25, 2024 at 5:59 AM