?
?
LiveJournal
  • Find more
    • Your 2020 in LJ
    • Communities
    • RSS Reader
  • Shop
  • Help
  • Login
  • CREATE BLOG Join
  • English (en)
    • English (en)
    • Русский (ru)
    • Українська (uk)
    • Français (fr)
    • Português (pt)
    • español (es)
    • Deutsch (de)
    • Italiano (it)
    • Беларуская (be)
r6research —
Subscribe
LiveJournal

Log in

No account? Create an account
Forgot password
Facebook Twitter Google RAMBLER&Co ID

By logging in to LiveJournal using a third-party service you accept LiveJournal's User agreement

No account? Create an account

r6research

  • Recent Entries
  • Friends
  • Profile
  • Archive
  • Tags
  • Categories
  • Memories
← →
18th
  • 10:15 pm Prisms! - 4 comments
Collapse

Calendar

Jun 2019
S M T W T F S
            1
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30            

Tags

  • clear
  • coalgebra
  • comonad
  • coq difficulties
  • galois theory
  • lens
  • mathscheme

Comments

  • ex_juan_gan
    31 Dec 2015, 04:19
    From Van Laarhoven Isomorphisms in one shot.
    Categorically, it's pretty trivial, take the cone, tweak it a little bit.
  • r6research
    25 Nov 2015, 04:59
    Grate: A new kind of Optic
    We can also build an optic for finite Naperian containers (a.k.a. finite vectors).

    ∃ x y n. (s → x n) × Iso(a,b) x y × (y n → t)
    =
    ∃ x y n. (s → x n) ×…
  • r6research
    23 Nov 2015, 03:56
    A Representation Theorem for Second-Order Pro-functionals
    Okay the isomorphism between FreeStrong and Pastro is

    Pastro p s t
    =
    ∃ x y z. (s → (x × z)) × p x y × ((y × z) → t)
    ≅ [ defining adjunction for ×…
  • r6research
    22 Nov 2015, 15:45
    A Representation Theorem for Second-Order Pro-functionals
    xplat suggests that FreeStrong and Pastro are isomorphic.

    The conjectured isomorphism would be

    > toFreeStrong (Pastro l m r) = FreeStrong (dimap (fst . r) (\y a -> l (y, (snd (r a)))) m)
    >…
  • Julien Truffaut
    23 Sep 2014, 18:58
    Mainline Profunctor Heirarchy for Optics
    Hi Edward,

    I don't see how to implement traversal with your definition of Walk, would you mind to give me an hint?

Search