Comments on A Neighborhood of Infinity: Infinitesimal Types

I also see a connection to the boundary operator o...

2011-07-16T08:35:56.530-07:00

I also see a connection to the boundary operator on chains in algebraic topology:
http://en.wikipedia.org/wiki/Chain_%28algebraic_topology%29

The d^2 = 0 is also the case of the exterior deriv...

2011-07-16T08:31:14.526-07:00

The d^2 = 0 is also the case of the exterior derivative for differential forms:
http://en.wikipedia.org/wiki/Differential_form#Exterior_differential_complex

Snorri, I did eventually come up with an interpre...

2011-03-17T13:35:29.449-07:00

Snorri,

I did eventually come up with an interpretation of D^2=0 for types. See here.

Hmm. Reminds me of monads in Haskell.

2011-03-17T13:32:32.078-07:00

Hmm. Reminds me of monads in Haskell.

I don't suppose there's anything even rese...

2009-11-22T23:12:12.072-08:00

I don't suppose there's anything even resembling singleton types in Haskell…is there?

d^0 = 0 corresponds to "get rid of the constants"....

2008-05-21T13:50:00.000-07:00

d^0 = 0 corresponds to "get rid of the constants". Ideas are now forming in my brain but I don't know if they'll go anywhere.

Linear logic also bans contraction. This correspon...

2008-05-21T02:38:00.000-07:00

Linear logic also bans contraction. This corresponds to not being able to avoid using the hole. Or perhaps that corresponds to weakening. I forget whether I'm going forwards or backwards.
In any case, is it so that d^0 = 0 rather than 1?