Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings

[Martin Baker]

On 6/25/19, William Sit<address@hidden>  wrote:
> The expression  x = x + 0, whether treated as a type or an equation,
> can only make sense when x, =, + and 0 are clearly typed and defined.
> It makes little sense to me that this, as an equation, can be "proved"
> to be valid universally (that is, without the definition of, say +).

If x is a natural number defined like this in Coq:

Inductive nat : Set := O : nat | S : nat -> nat

then x = x + 0 is not an axiom but is derivable.
Of course this all depends on the structures and definitions, I didn't 
mean to imply that it is valid universally.

On 25/06/2019 19:28, Tim Daly wrote:
> The "elegant way" that Martin is questioning is the problem
> of combining a certain kind of logic operation (refl aka
> "reflection" where both sides are equal) with the notion of
> a mathematical unit.

I think that refl (short for "reflexivity" of = relation), is the usual 
abbreviation for the only constructor of an equality type in Martin-Lof 
type theory.

I get the impression that this theory is very powerful in proof 
assistants and I am questioning if you proposing to build this into 
Axiom and how?

Martin