⚠️ This module is not part of this project and is only included for reference.
It is either part of the 1lab, the cubical library, or a built-in Agda module.
```agda module Data.Sum where ``` # Sum types ```agda open import Data.Sum.Properties public open import Data.Sum.Base public ```