pisigma-0.2: examples/Conat.pi

:l Empty.pi
:l Unit.pi

CoNat : Type;
CoNat = (l : { z s }) * case l of {
                           z -> Unit
			 | s -> Rec [^ CoNat] };


zero : CoNat;
zero = ('z,'unit);

succ : ^CoNat -> CoNat;
succ = \ n -> ('s,fold n);

one : CoNat;
one = succ [zero];

two : CoNat;
two = succ [one];

omega : CoNat;
omega = succ [omega];


add : CoNat -> CoNat -> CoNat;
add = \ m n -> split m with (lm , m') ->
                 case lm of {
		     z -> n
 		   | s -> succ [add (! (unfold m')) n] };

EqCoNat : CoNat -> CoNat -> Type;
EqCoNat = \ m n -> split m with (lm , m') ->
              split n with (ln , n') ->
                   case lm of {
		     z -> case ln of {
		             z -> Unit
			   | s -> Empty }
	           | s -> case ln of {
		             z -> Empty
			   | s -> Rec [^ (EqCoNat (! (unfold m')) (! (unfold n')))]}};


reflCoNat : (n:CoNat) -> EqCoNat n n;
reflCoNat = \ n -> split n with (ln , n') ->
       	          case ln of {
		     z -> 'unit
		   | s -> fold [reflCoNat (! (unfold n'))] };

symCoNat : (m n:CoNat) -> EqCoNat m n -> EqCoNat n m;
symCoNat = \ m n p ->
              split m with (lm , m') ->
              split n with (ln , n') ->
                   case lm of {
		     z -> case ln of {
		             z -> 'unit
			   | s -> case p of {}}
	           | s -> case ln of {
		             z -> case p of {}
			   | s -> fold [symCoNat (! (unfold m')) (! (unfold n')) (! (unfold p))] }};

transCoNat : (l m n:CoNat) -> EqCoNat l m -> EqCoNat m n -> EqCoNat l n;
--transCoNat = \ l m n p q ->
	   

{-
subst : (P : CoNat -> Type)
      -> (m : CoNat) -> (n : CoNat)
      -> (EqCoNat m n)
      -> P m -> ^ (P n);
subst = \ P m n q x ->
              split m with (lm , m') ->
              split n with (ln , n') ->
                 case lm of {
		     z -> case ln of {
		             z -> case m' of {
			             unit -> case n' of {
				                unit -> [x] }}
			   | s -> case q of {}}
	           | s -> case ln of {
		             z -> case q of {}
			   | s -> [unfold m' as m' ->
                                   unfold n' as n' ->
                                   subst (\ i -> P (succ [i])) (! m') (! n') (! q) x]}};
-}

{- seems we need an eliminator for boxes, e.g. unbox
-}