Natural Order definition utilizing an identity type

[biocini]

Quoting from the preamble:

Following the equality case of the triangle inequality, we can define a
partial order on ℕ directly with an identity type, namely by considering
the fixed points of the family of functions indexed by x of the form (λ y
→ ∣ y - x ∣ + x). This is because the only inhabitants of these fixed
point equalities are identities where x is less than or equal to y. And
because ℕ is a set, each term of this identity type thereby becomes a
proposition, although in contrast to the standard order definition based
on 𝟙 each inhabitant of our order type is its own distinct refl term and
hence distinct inequalities will not be equal terms.

In hindsight it is obvious a type such as this ought to be possible,
because the definition for the standard order module essentially
calculates the inhabitation of its type by the same recursion algorithm as
absolute difference, with the provision that the succ x ≤ zero case is
defined as the empty type. Our definition leads to a partial order type
with interesting properties. As opposed to the one generated by a function
from ℕ to 𝟙, we are able to work directly with the identifications that
specify the order relation, so 'succ-lc' for example will translate an
inequality of 'succ m ≼ succ n' to 'm ≼ n', and likewise with 'ap succ'
for the other direction. Negation is directly handled by the standard
negation proofs for the Naturals. The use of transport is ergonomic as
each term is directly an identity term. Our type definition also has
strong computational properties that assist Agda's case matching as
opposed to the standard definition; you will never see it attempt to match
for the case 'succ x ≼ zero' as Agda can automatically detect this type
is uninhabited.

We use the curly order '≼' so as not to conflict with the one already
defined for the Naturals. Although the early portions of this module were
written myself, after I translated Escardo's definition of ≤-induction to
this type I decided to go further and have begun translating all the Order
lemmas in the standard module to accommodate this definition. For the most
part, I have attempted to preserve the titles and type definitions
exactly, but in the earlier sections of the modules I took some liberties
as I wanted to tailor the most fundamental lemmas to the character of this
type, and also to make certain operations more ergonomic and reduce the
character count of proofs. Notably, 'equal-gives-less-than-or-equal' is
simply '≼-＝' here.

Aside from the fundamental lemmas as well as ones concerning absolute
difference the credit for most of the type definitions that will be listed
here goes to the efforts of Martin Escardo, Tom de Jong, and Andrew Sneap.
Sometimes I needed to tailor their proofs to fit our order definition, but
in many cases I was able to use essentially the same principles from
proofs in the other module to guide the equivalent proofs here.

[biocini]

corrected a small mistake in the preamble, as well as adding to the index file if this is suitable

[martinescardo]

Thanks for your contribution. I am sorry for the delay. I had forgotten about this.

One more thing: although many parts of TypeTopology use zero, I favour using 0 nowadays, so if you adopt this, it would be great.

[martinescardo]

Could you rename ≼-＝ to `≼-gives-＝' please?

[martinescardo]

I am not sure why you are proving ≼-is-discrete and ≼-is-set. For the latter you could use props-are-sets. Do you really need this? I would suggest to delete both.

[martinescardo]

Please rename this to ＝-gives-≼ y.

[martinescardo]

I would omit the definition in line 186. It is just the contrapositive of the previous one, and we have a definition of contrapositivity in MLTT.Negation.

[martinescardo]

Please use alphabetical order in the index imports.

[biocini]

I will be implementing these changes after I finish my work for the Modular Group. I've been thoughtful about this module more generally and how I want to structure it. First I was considering the question of under what general conditions it is possible to construct a type equivalence like this, and it seems directly related to the fundamental theorem of identity types, so I'm giving some thought of how to explore that theme in this module.

[ayberkt]

I will be implementing these changes after I finish my work for the Modular Group.

@lane-core I’ve converted this to a draft PR since you mentioned that you will be addressing the review after PR #214 is completed.

[biocini]

@ayberkt @martinescardo to update here, a simpler presentation of this idea would use the identity type formed by monus m n = 0 as our definition. But yes, I will address this module after my work in PR #214

[martinescardo]

Is there any intention to continue with this?

[biocini]

@martinescardo I will revisit this one in more depth after the Modular Group PR, as I want to give this idea some reconsideration in light of what I've learned since making the original request. For now I can accommodate your requested changes and get it off the TT PR stack, and submit a new PR when I decide to revise.