{- \begin{verbatim} Time-stamp: "1997-10-13 11:59:43 peter" #include "./standard.half" #include "./Boole.half" \end{verbatim} \newcommand{\defocc}[1]{\framebox{\emph{#1}}} % Defining occurrence How to organise the `facilities' for simple structures? Take `worlds' as an example. \tableofcontents -} {- \section{ Theory of worlds } A \defocc{world} consists of a set, and a predicate defined on it. Think of the elements of the domain set as propositions (or types), and the predicate as a truth predicate. By the Curry-Howard correspondence, we can also think of the predicate as a set valued family indexed by the base set. The set corresponding to a proposition is the set of its proofs, and to say that the proposition is true is to say the set has an element. So we can say that the notion of a world is a constructive formulation of what from the classical point of view would be described as a set (of formal propositions) together with a subset of it (the formally provable propositions). It is a much richer notion constructively, because we have a much richer notion of `truth-value' (of course, one can express this constructively as well, with labour). The interest of worlds is largely that they can function as formal universes - that is, they can in many situations play the role of the framework's (large) universe: \par \begin{tabular}{l} \texttt{ Set : Type } \\ \texttt{ El = \ s -> s : ( s : Set )-> Type } \end{tabular} \newline yet they are small, and mathematically managable: \par \begin{tabular}{l} \texttt{ set : Set } \\ \texttt{ el = \ s -> el s : ( s : El set )-> Set }. \end{tabular} -} World = theory { t = {- the type of a world -} Fam Set : Type , m ( U : Set, T : Pow U ) = {- how to make a world -} struct { I = U, g = T } : t , example0 = m empty.set (empty.fun Set) : t , example1 ( given : t ) = {- Von Neumann successor -} m (maybe given.I) (\ a -> case a of { $fail -> given.I , $unit a1 -> given.g a1 } ) : t , f ( us : Fam t ) = let { I = us.I : Set , g = us.g : ( i : I )-> t , U = \i->(g i).I : Pow I , T = \i -> (g i).g : ( i : I)-> Pow (U i) } in theory { sum = m (Sigma I U) (\iu->T iu.p iu.q) : t , prod = m (Pi I U) (\i2u -> Pi I (\i->T i (i2u i))) : t } : Theory , i ( me : t ) = {- attributes and properties of a single instance -} theory { {- standard names for the components -} U = me.I : Set , T = me.g : Pow U , inhabited = sig { witness : U , proof : T witness } : Set , inconsistent = ( a : U )-> T a : Set , {- World.i me -} {- keeping the set \texttt{U} fixed. -} lattice ( T' : Pow U ) = theory { ops ( a : U ) = theory { cap = and (T a) (T' a) : Set , cup = or (T a) (T' a) : Set , subseteq = arrow (T a) (T' a) : Set , supseteq = arrow (T' a) (T a) : Set } : Theory {- (World.i me).lattice.ops a -} , LE = ( a : U )-> (ops a).subseteq : Set , GE = ( a : U )-> (ops a).supseteq : Set , EQ = sig { le : LE, ge : GE } : Set , cap = \ a -> (ops a).cap : Pow U , cup = \ a -> (ops a).cap : Pow U , exhaustive = ( a : U )-> (ops a).cup : Set , disjoint = ( a : U )-> empty.set : Set , consistent = sig { witness : U , proof : (ops witness).cap } : Set , END = [] : [] } : Theory {- (World.i me).lattice -} {- some more sanitary formulations -} , LE = \ T' -> (lattice T').LE : Quantifier U , GE = \ T' -> (lattice T').GE : Quantifier U , EQ = \ T' -> (lattice T').EQ : Quantifier U , cap = \ T' -> (lattice T').cap : OP (Pow U) , cup = \ T' -> (lattice T').cap : OP (Pow U) , complement = \a->( a : U )-> empty.set : Pow U , {- World.i me -} binary ( other : t ) = {- things to do with 2 worlds -} let { U' = other.I : Set , T' = other.g : Pow U' } in theory { To = {- set of maps from me to other -} sig { u : fun U U' , t : Pi U (\x->fun (T x) (T' (u x))) } : Set , From = {- set of maps from other to me -} sig { u : fun U' U , t : Pi U' (\x->fun (T' x) (T (u x))) } : Set , add = m (or U U') (\a'->case a' of { $inl a -> T a, $inr b -> T' b}) : t , mul = m (and U U') (\a->and (T a.p) (T' a.q)) : t } : Theory {- (World.i me).binary -} , {- World.i me -} {- some convenient forms: \texttt{(World x).i.Maps.To y} -} Maps = theory { To = {- returns set of maps to another world -} \ other -> (binary other).To : Pow t , From = {- returns set of maps from another world -} \ other -> (binary other).From : Pow t } : Theory {- (World.i me).Maps -} , it = me : t } : Theory {- World.i me -} } : Theory {- World -} , World' {- Merging into above -} ( A : Set, B : Pow A ) {- components of a world. -} = {- Something to be merged in -} theory { Inhabited = Sigma A B : Set {- B is a non-empty predicate -} , Universal = Pi A B : Set {- B holds universally -} {- We can think of A as a small universe of sets, -} {- and B as its decoding function. This leads to -} {- a number of definitions. -} , Relative = theory { set = A : Set , el = B : Pow set , pow = \ X -> ( x : X )-> set : OP Set , pow' = \ s -> pow (el s) : ( s : set )-> Set , fam = \ X -> sig { d : set , p : ( i : el d )-> X } : OP Set , rel = \ X -> ( x : X )-> pow X : OP Set , ts = \ X -> ( x : X )-> fam X : OP Set , quant = \ X -> pow (pow X) : OP Set , famfam = \ X -> fam (fam X) : OP Set , pands = \ X -> ( x : X )-> famfam X : OP Set } : Theory {- the `subseteq' relation -} , LE = \ B' -> ( a : A , hyp : B a )-> B' a : Pow (Pow A) , GE = \ B' -> ( a : A , hyp : B' a )-> B a : Pow (Pow A) , EQ = \ B' -> and (LE B') (GE B') : Pow (Pow A) {- binary operations -} , cap = \ B' a ->and (B a) (B' a) : OP (Pow A) , cup = \ B' a ->or (B a) (B' a) : OP (Pow A) {- operations on families of predicates -} , Cap ( B' : Fam (Pow A) ) = \a->Pi B'.I (\i->B'.g i a) : Pow A , Cup ( B' : Fam (Pow A) ) = \a->Sigma B'.I (\i->B'.g i a) : Pow A {- a universe containing this world, closed under a quantifier -} , QClosure ( Q : (A : Set)-> Quantifier A ) = let { Phi ( x : World.t ) {- the operator we fix -} = let { wx = World.i x : Theory, U = wx.U : Set, T = wx.T : Pow U } in World.m ( data { $A {- code for this world -} , $B ( a : A ) {- codes for the sets in this world -} , $Q {- codes for sets of quantifier form -} ( domain : U , predicate : ( x : T domain )-> U ) } ) ( \ u -> case u of { $A -> A , $B a -> B a , $Q d p -> Q (T d) (\ a -> T (p a)) } ) : World.t , x = Phi x : World.t } in x : World.t , QClosureOP( Q : ( A : Set )-> Quantifier A) = {- throws in one level of the quantifier -} \ AB -> let { A = (World.i AB).U : Set , B = (World.i AB).T : Pow A , A'= data { $already_there ( a : A ) , $q ( a : A , b : ( x : B a )-> A ) } : Set , B'= \ u -> case u of { $already_there a -> B a , $q a b -> Q (B a) (\ x -> B (b x)) } : Pow A' } in World.m A' B' : OP (World.t) {- fixed point of this is closed under Q -} } : Theory {- \subsection{Debris} -} {- This belongs with the world stuff. Already there? -} , SuccU {- Successor of a family -} ( AB : Fam Set ) = let { A = AB.I : Set , B = AB.g : ( a : A )-> Set } in struct { I=data{ $0, $1 ( a : A )} , g=\i->case i of { $0 -> A , $1 a1 -> B a1 } } : Fam Set {- Least family of sets extending a given family, and closed under an operator from families of sets to families of sets. -} {- belongs with world stuff -} , SuperU ( F : ( X : Fam Set )-> Fam Set , AB : Fam Set ) = let { VS = let { V = VS.I : Set , S = VS.g : ( v : V )-> Set , G ( a : V, b : ( i : S a )-> V) = F (struct { I=S a , g=\i->S (b i)}) : Fam Set , U ( a : V, b : ( i : S a )-> V) = (G a b).I : Set , T ( a : V, b : ( i : S a )-> V) = (G a b).g : ( u : U a b )-> Set } in struct { I=data { $0 , $1 ( a : AB.I ) , $u ( a : V , b : ( i : S a )-> V ) , $t ( a : V , b : ( i : S a )-> V , c : U a b ) } , g=\i->case i of { $0 -> AB.I , $1 a -> AB.g a , $u a b -> U a b , $t a b c -> T a b c } } : Fam Set } in VS : Fam Set , mark = [] : []