r6research

No account? Create an account

Remember me

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

← →

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?