(2-2. Interpret disjoint union types A + B in the groupoid model.)

(2-3. Does the D-sets model validate or refute the Law of Excluded Middle
      (P : Prop) -> P + ¬ P? (We can interpret Prop = modest sets))

3-1. Extend the (sketch of the) canonicity proof to also show the Disjunction Property of type theory: if P + Q is provable, then P is provable or Q is provable.