Re: [Axiom-developer] Proving Axiom Correct, "state of the art" report

[Martin Baker]

On 31/03/17 05:34, Tim Daly wrote:
> Consider the Axiom Domain NonNegativeInteger. NNI roughly
> corresponds to the Type theory "Nat" construction. They differ
> in that Axiom uses Lisp Integers whereas Type theory uses
> Peano arithmetic (a zero and a successor function) but for
> our purposes this does not matter at the moment.

Perhaps there are issues around this that will matter? Given that there 
are two formulations of each algebra, one like this:

zero: () -> $
succ: ($) -> $

and one like this:

+ ($,$) -> $

If one form is needed for inductive proofs and the other form for 
applied mathematics. Could Axiom hold both forms in a single 
category/domain and switch between them as needed?

Martin