type-settheory- Sets and functions-as-relations in the type system






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 NStructures


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 NStructures, in other words, that it is isomorphic to the natural numbers


NInitial :: (forall z2 set2 succ2. ExUniq1 (NMorphism set1 z1 succ1 z2 set2 succ2)) -> NInitial set1 z1 succ1 

data TNat z s whereSource

Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let's call these TNats


IsZ :: TNat z s z 
IsS :: TNat z s n -> TNat z s (s n) 

data Succ z s whereSource

Successor function made from a unary type constructor


Succ :: (n :∈: TNat z s) -> Succ z s (n, s n) 

succFun :: (TNat z s :~>: TNat z s) (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)


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) 

initorFun :: forall z s set2 z2 succ2. NStructure set2 z2 succ2 -> (TNat z s :~>: set2) (Initor z s z2 succ2)Source