back to index Equations Inline Footnotes module Data.Sum where Sum Types🔗 open import Data.Sum.Properties public open import Data.Sum.Base public