Entries from 2017-10-09 to 1 day
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 が返る…