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

Type.Nat

Description

TODO

• Prove that `Initor` is an `NMorphism`
• Prove that it is uniquely so

Synopsis

# Documentation

data NStructure set z succ whereSource

Sets equipped with a constant and a function to itself

Constructors

 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

Constructors

 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

Constructors

 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

Constructors

 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

Constructors

 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`)

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)

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