instance
  bin-union-set
   : ∀ {x y} ⦃ _ : set x ⦄ ⦃ _ : set y ⦄
   → set (x ∪ y)
  bin-union-set {x} {y}
   = set (∐ ⟨ x , y ⟩)
   $ (λ z → #> λ u → *> λ zu
   → (λ { equal → inl zu })
   ∥ (λ { equal → inr zu }))
   E λ z
   → (λ zx → x # zx * inl equal)
   ∥ (λ zy → y # zy * inr equal)