is ∃f monadic?!

[Vlad Patryshev]

Hi,

I never thought of it before, but it seems like ∃f functor is actually monadic (making it pretty legal for Scala Set to be covariant, in a way). Can anybody please say I am wrong?

--
Thanks,
-Vlad

[Vlad Patryshev]

Hi,

I know what a monad is; and yes, the issue is - which category. I was not talking about formulae and proofs, I meant a general elementary topos. It should be a good environment for modeling.

2009/8/1 Meredith Gregory <lgreg.m...@gmail.com>

Vlad,

To identify a monad you to say at least what the category is and the action of the endofunctor. Is the category the one in which the objects are formulae and the morphisms are proofs? Already that's a bit problematic. Maybe the objects are pairs (formula,variable)? Anyway, once you say what the set up is, you only need to supply the unit and mult natural isomorphisms and then check coherence.

More formally, a monad is a triple consisting of

• an endofunctor, T : C -> C
• a natural transformation unit : C -> TC
• a natural transformation mult : TTC -> TC
  

You need to check that

• T mult ; mult = mult T; mult
• if T is an analog of a compositing operation, this is the analog of associativty
  
• unit T; mult = T unit; mult
• if T is an analog of a compositing operation, this is the analog of specifying an identity element
  

Your job, should you chose to accept it, is to say what the category, unit and mult are -- since you've already given the candidate endofunctor -- and check those conditions. You might find this reference helpful.

Best wishes,

--greg

On Sat, Aug 1, 2009 at 9:16 AM, Viktor Klang <viktor...@gmail.com> wrote:

On Sat, Aug 1, 2009 at 3:43 AM, Vlad Patryshev <vpatr...@gmail.com> wrote:

Hi,

I never thought of it before, but it seems like ∃f functor is actually monadic (making it pretty legal for Scala Set to be covariant, in a way). Can anybody please say I am wrong?

You're wrong?
Happy?
 

--
Thanks,
-Vlad

--
Viktor Klang

Rogue Scala-head

Blog: klangism.blogspot.com
Twttr: viktorklang

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com

--
Thanks,
-Vlad