Is a merge interval function available?

[Peng Yu]

I'm wondering there is already a function in python library that can
merge intervals. For example, if I have the following intervals ('['
and ']' means closed interval as in
http://en.wikipedia.org/wiki/Interval_(mathematics)#Excluding_the_endpoints)

[1, 3]
[2, 9]
[10,13]
[11,12]

I want to get the following merged intervals.

[1,9]
[10,13]

Could somebody let me know if there is a function in the python
library?