Koji Miyazato

@viercc.bsky.social

38 Followers 61 Following

Twitter(X), GitHubなどにいるのと同一人物です openpgp4fpr:B2E1DC9AF16599BD2D873A227BABC58075EC4EE6 興味: Haskell, 数学

(screenshot of AI chat service, user's input)
やった！それは私が意図した通りです。

より読みやすかったり、整理された証明とするために、

* そもそも証明の流れとして整理すべき箇所

* Agdaで記述された証明としてidiomaticでない箇所

を探していただけますか？

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

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

$-- 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`.$

$Screenshot showing how three "dot symbols" shows on my editor. | \cdot ····· | \. ∙∙∙∙∙ | \bullet ••••• surrounded by line repeated vertical bar character (||||||...)$

$-- 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`.$

$-- 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 }$

（Googleの検索結果のスクリーンショット）
タイトル:「群の作用する可換紙の上の即戦」

(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)

$(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))$

$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))$

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)
```

$WV \to W \\ WV \to V \\ WV \to VVW \\ WV \to VWW$

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

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)

$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 = (+))$

$-- 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$

$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)$

${-# 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)$