the meeting of March 28, 2012

[Vlad Patryshev]

There were just Larry and me.

We gleaned (is this the right verb?) over Alex' paper re: arrows, looked into arrows as defined in Haskell, then switched the topic.

I had recently found a nice boolean 2-valued topos with an example of a monad that is not applicative. It is Set^Z2 (s ets with an action of Z2 group).

The problem we were trying to solve is expressing this topos, or this logic, in the terms of types. The types would be sets, like in Hask, but with an attached involution. Sure functions should preserve involution.

While Larry had gradually moved to the idea of having involution defined on types (not on type members), we have not come to any definite theory.

I wonder if anybody knows anything.

This topos, Set^Z2 is especially interesting because it is boolean, but without the AC. So there. Seems like AC, in a weak form probably, is required for the applicativity of monads. Cannot prove though.

Thanks,
-Vlad

[Larrytheliquid]

Thanks for the summary Vlad, this was a very fun meeting :)

--
You received this message because you are subscribed to the Google Groups "Bay Area Categories And Types" group.
To post to this group, send email to ba...@googlegroups.com.
To unsubscribe from this group, send email to bacat+un...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/bacat?hl=en.

--
Respectfully,
Larry Diehl

[Jason Dusek]

2012/3/30 Vlad Patryshev <vpatr...@gmail.com>:

> There were just Larry and me.

"It was just Larry and me."

> We gleaned (is this the right verb?) over Alex' paper...

"We looked over Alex's paper..."

--
Jason Dusek
pgp // solidsnack // C1EBC57DC55144F35460C8DF1FD4C6C1FED18A2B

[Arthur Chan]

D00d...

Arthur :: LittleBrick