module Type.Nat where
import Type.Set
import Type.Dummies()
import Type.Function
import Type.Logic()
import Data.Type.Equality
import Control.Monad()
import Control.Exception
#include "../Defs.hs"
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 :: SET) 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 :: SET where
IsZ :: TNat z s z
IsS :: TNat z s n -> TNat z s (s n)
data Succ z s :: SET where
Succ :: n :∈: TNat z s -> Succ z s (n,s n)
succFun :: (TNat z s :~>: TNat z s) (Succ z s)
succFun = IsFun (Subset (\(Succ n) -> n :×: IsS n))
(ExSnd . Succ)
(\(Succ _) (Succ _) k -> k)
tyconNStruct :: NStructure (TNat z s) z (Succ z s)
tyconNStruct = NStructure IsZ succFun
data Initor z s z2 succ2 :: SET 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)
initorFun (NStructure z2 succ2) =
let
prelation :: pair :∈: Initor z s z2 succ2 ->
pair :∈: TNat z s :×: set2
prelation InitorZ = IsZ :×: z2
prelation (InitorS i0 p) = case prelation i0 of
q1 :×: _ ->
IsS q1
:×:
inCod succ2 p
ptotal :: n :∈: TNat z s -> ExSnd (Initor z s z2 succ2) n
ptotal IsZ = ExSnd InitorZ
ptotal (IsS n) =
case ptotal n of
ExSnd (inn2 :: Initor z s z2 succ2 (n,n2)) ->
(let
succ2ofn2 :: ExSnd succ2 n2
succ2ofn2 =
case prelation inn2 of
_ :×: n2 ->
total succ2 n2
in
case succ2ofn2 of
ExSnd e -> ExSnd (InitorS inn2 e))
psval :: Initor z s z2 succ2 (n,n2) ->
Initor z s z2 succ2 (m,m2) ->
n2 :=: m2
psval InitorZ InitorZ = Refl
psval (InitorS inn2 succ2n2) (InitorS inn2' succ2'n2') =
case psval inn2 inn2' of
Refl ->
case sval succ2 succ2n2 succ2'n2' of
Refl -> Refl
psval (InitorS _ _) InitorZ = assert False undefined
psval InitorZ (InitorS _ _) = assert False undefined
in
IsFun (Subset prelation) ptotal (\p1 p2 k -> case psval p1 p2 of
Refl -> k)