ski 2017-02-01 16:45:58
"Elementary Categories, Elementary Toposes" by Colin McLarty in 1992 describes how the internal language in a topos works
mniip 2017-02-01 16:48:10
[13:50:12] ... it'd be interesting to see how something like this could apply to, or compare to, an internal language in a cartesian closed category, or monoidal closed, or whatever (or some weaker variant, e.g. without closedness)
ski 2017-02-01 16:48:59
ah, ok
ski 2017-02-01 16:49:22
what was the date of that ?
mniip 2017-02-01 16:50:07
2017/01/24
ski 2017-02-01 16:51:48
mniip : it was in response to "Re »other than people's expectations«, I remember hearing that Applicative is mathematically not a »superclass« of Monad – they're orthogonal concepts, and only in the special case of Hask(ell) they come together in a hierarchy."
mniip 2017-02-01 16:52:36
are you talking about two different monoidal categories on top of End(Hask)?
ski 2017-02-01 16:52:59
so i was wondering whether one could express `Monad' and `Applicative' in such a setting, and whether in that case a monad needn't be an idiom
mniip 2017-02-01 16:53:52
well, I have a snippet of code over here that expresses Monad and Applicative as Monoids in two different Monoidal categories
ski 2017-02-01 16:54:29
i'm not quite sure what i would be talking about
ski 2017-02-01 16:55:35
i was wanting some way to express it categorially, such that the internal language would *look* like "the Haskell situation", more or less
mniip 2017-02-01 17:17:55
ski, what *is* an internal language
Squarism 2017-02-01 17:18:27
theres no fmap ( mapFst / mapSnd ) for tuples? I have some memory there was?
mniip 2017-02-01 17:18:43
Squarism, Control.Arrow.first and second
mniip 2017-02-01 17:18:47
also ***
Squarism 2017-02-01 17:19:01
oh ok
mniip 2017-02-01 17:19:02
also fmap works on the second tuplee
nshepperd 2017-02-01 17:19:08
also bifunctor
Squarism 2017-02-01 17:19:22
thanks
erisco 2017-02-01 17:20:14
so I'm really wishing SOrd gave you the equality proof… what a PITA
erisco 2017-02-01 17:33:33
all I want to do right now is find the TestEquality instance for Sing Nat
erisco 2017-02-01 17:35:27
sorry I guess that'd be Sing (SNat n)
erisco 2017-02-01 17:36:42
or is it Sing Nat
erisco 2017-02-01 17:36:48
I am going a bit crazy
EvanR 2017-02-01 17:37:09
"s(n) = s(m) only if n = m", does the "only if" here mean the same thing as "->"
EvanR 2017-02-01 17:37:23
and just "if" would mean <- ?
EvanR 2017-02-01 17:37:36
or
EvanR 2017-02-01 17:38:03
or should it be if and only if
erisco 2017-02-01 17:38:04
maybe it is short for double implication
EvanR 2017-02-01 17:38:28
s is a function so that would be redundant
erisco 2017-02-01 17:39:47
this is why I use the symbols when I can
nshepperd 2017-02-01 17:42:49
EvanR: I assume yes. 's(n) = s(m) -> n = m' gives injectivity
nshepperd 2017-02-01 17:43:48
the other way 'n = m -> s(n) = s(m)' is really the definition of s being a function, so that would generally be true always
