title: Do Hask or Agda have equalisers?
body: <p>I was somewhat undecided as to whether this was a math.SE question or an SO one, but I suspect that mathematicians in general are fairly unlikely to know or care much about this category in particular, whereas Haskell programmers might well do.</p>
  
  <p>So, we know that <strong>Hask</strong> has products, more or less (I'm working with idealised-Hask, here, of course). I'm interested in whether or not it has equalisers (in which case it would have all finite limits).</p>
  
  <p>Intuitively it seems not, since you can't do separation like you can on sets, and so subobjects seem hard to construct in general. But for any specific case you'd like to come up with, it seems like you'd be able to hack it by working out the equaliser in <strong>Set</strong> and counting it (since after all, every Haskell type is countable and every countable set is isomorphic either to a finite type or the naturals, both of which Haskell has). So I can't see how I'd go about finding a counterexample.</p>
  
  <p>Now, Agda seems a bit more promising: there it <em>is</em> relatively easy to form subobjects. Is the obvious sigma type <code>Σ A (λ x → f x == g x)</code> an equaliser? If the details don't work, is it <em>morally</em> an equaliser?</p>