|
|
|
Description |
TODO
|
|
Synopsis |
|
|
|
Documentation |
|
data NStructure set z succ where | Source |
|
Sets equipped with a constant and a function to itself
| Constructors | |
|
|
data NMorphism set1 z1 succ1 set2 z2 succ2 f where | Source |
|
Structure-preserving maps of NStructures
| Constructors | |
|
|
data NInitial set1 z1 succ1 where | Source |
|
Expresses that (set1,z1,succ1) is initial in the cat of NStructures, in other words, that it is isomorphic to the natural numbers
| Constructors | |
|
|
|
Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let's call these TNats
| Constructors | |
|
|
|
Successor function made from a unary type constructor
| Constructors | |
|
|
|
|
|
|
data Initor z s z2 succ2 where | Source |
|
The unique morphism from an TNat to any NStructure
NB: s is a type constructor, but succ2 is a Function (IsFun)
| Constructors | InitorZ :: Initor z s z2 succ2 (z, z2) | | InitorS :: Initor z s z2 succ2 (n1, n2) -> ((n2, sn2) :∈: succ2) -> Initor z s z2 succ2 (s n1, sn2) | |
|
|
|
|
|
Produced by Haddock version 2.4.2 |