type-settheory-0.1.2: Type-level sets and functions expressed as typesSource codeContentsIndex
Type.Nat
Description

TODO

Synopsis
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
NInitial :: (forall z2 set2 succ2. ExUniq1 (NMorphism set1 z1 succ1 z2 set2 succ2)) -> NInitial set1 z1 succ1
data TNat z s where
IsZ :: TNat z s z
IsS :: TNat z s n -> TNat z s (s n)
data Succ z s where
Succ :: (n :∈: TNat z s) -> Succ z s (n, s n)
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
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)
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 NStructures
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 NStructures, 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
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)

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
Produced by Haddock version 2.4.2