Home/Mathematics/Category Theory and Functional Programming/

Types

100%

Sum Types

Introduction, elimination and computation rules

Data constructors as functions (morphisms), in this case from the terminal object (since they are nullary).

Big enumerations

Case statement as an enumeration elimination pattern

Pattern matching as an enumeration elimination rule

Nullary data constructors as the enumeration introduction rule

Functions (computation rules) from Either

Functoriality/lifting for sum types

Introduction, elimination and computation rules

Appears in 2 boards

Types
Bool

Appears in 2 boards

Types
Either

Product Types

Functoriality/lifting for products

Function Types

Function application as the elimination rule for function types