- data NStructure set z succ where
- NStructure :: (z :∈: set) -> (set :~>: set) succ -> NStructure set z succ
- data NMorphism set1 z1 succ1 set2 z2 succ2 f where
- NMorphism :: NStructure set1 z1 succ1 -> NStructure set2 z2 succ2 -> (set1 :~>: set2) f -> (f z1 :=: z2) -> ((f :○: succ1) :==: (succ2 :○: f)) -> NMorphism set1 z1 succ1 z2 set2 succ2 f
- data NInitial set1 z1 succ1 where
- data TNat z s where
- data Succ z s where
- succFun :: (TNat z s :~>: TNat z s) (Succ z s)
- tyconNStruct :: NStructure (TNat z s) z (Succ z s)
- data Initor z s z2 succ2 where
- initorFun :: forall z s set2 z2 succ2. NStructure set2 z2 succ2 -> (TNat z s :~>: set2) (Initor z s z2 succ2)
Documentation
data NStructure set z succ whereSource
Sets equipped with a constant and a function to itself
NStructure :: (z :∈: set) -> (set :~>: set) succ -> NStructure set z succ |
data NMorphism set1 z1 succ1 set2 z2 succ2 f whereSource
Structure-preserving maps of NStructure
s
NMorphism :: NStructure set1 z1 succ1 -> NStructure set2 z2 succ2 -> (set1 :~>: set2) f -> (f z1 :=: z2) -> ((f :○: succ1) :==: (succ2 :○: f)) -> NMorphism set1 z1 succ1 z2 set2 succ2 f |
data NInitial set1 z1 succ1 whereSource
Expresses that (set1,z1,succ1)
is initial in the cat of NStructure
s, in other words, that it is isomorphic to the natural numbers
Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let's call these TNats
Successor function made from a unary type constructor
tyconNStruct :: NStructure (TNat z s) z (Succ z s)Source
data Initor z s z2 succ2 whereSource
The unique morphism from an TNat
to any NStructure
NB: s
is a type constructor, but succ2
is a Function (IsFun
)