<div dir="ltr">Hi,<div>At the meeting this past monday, I had said that sigma types were like cartesian products, and David corrected me that they are like disjoint unions, and I had to think for a bit before agreeing.  (They are actually colimits, because the indexing types are weak infinity groupoids, not sets.)  The reason is that, generally, when you talk about a disjoint union or a colimit, the indexing set is uninteresting.  On the other hand, in a sigma type, the indexing type is often the most interesting part.  It sounds very strange, perhaps bordering on the nonsensical, to say that you are taking the disjoint union of singleton sets, indexed by functions f : A -&gt; B.  On the other hand, it&#39;s perfectly natural to do this with a sigma type (and I usually think of inhabitants of a sigma type as pairs, just where the second can depend on the first, while I usually mentally throw away the indexing label of a disjoint union).</div>


<div><br></div><div>-Jason</div></div>