Imaginantia

思ったことを書きます

Entries from 2017-10-01 to 1 month

連結と単連結

HoTTの話。 や はもちろん連結。 は連結ではない (2点集合)。 は単連結で、 は単連結でない。 ごちゃごちゃしてるけど次元で整理すると単純。 は-連結で-連結でない は-連結で-連結でない は-連結で-連結でない

モノイド的構造

Monoid Ordering (文字列順序) () (自明) Any (or) All (and) Semigroupの一点モノイド化 (e*s = s = s*e) Last (Maybe a) First (Maybe a) Product Sum Endo Max (Ord, Bounded) Min (Ord, Bounded) Semigroup Void NonEmpty Last (a) First (a) Max (Ord) …

Yoneda / co-Yoneda

Data.Functor.Yoneda Data.Functor.Contravariant.Coyoneda Yoneda lemma : ∀ b. (a → b) → f b ≅ f a (f : Functor) co-Yoneda lemma : ∃ b. (a → b, f b) ≅ f a (f : Contravariant) 左から右に (a → b) として id を取れる。a = b より f b = f a が返る…