Eventually pointed sequences

[malarbol]

A lot of properties from #1378 follow the pattern

Σ ℕ (λ N → (n : ℕ) → leq-ℕ N n → X n)

This PR introduces this concept for sequences of types and a few applications: eventually equal sequences and eventually constant sequences.

[fredrik-bakke]

This property(!) should be phrased with existential quantification. You can call the untruncated thing something like a bound-modulus-eventually-pointed-sequence (open for suggestions)

[fredrik-bakke]

Actually, wouldn't this just be a modulus-eventually-pointed-sequence?

[malarbol]

This property(!) should be phrased with existential quantification. You can call the untruncated thing something like a bound-modulus-eventually-pointed-sequence (open for suggestions)

As we've seen in #1378, there's still some debate (I think) on when to use dependent pairs vs existential quantifications. I'm starting with the easy version. Maybe the truncated things could me called is-merely-eventually-XXX?

[fredrik-bakke]

You're free to use the easy version, I'm just saying that it does not deserve the name is-eventually-pointed-sequence, and that a more fitting name for the thing you're defining is modulus-eventually-pointed-sequence since every eventually pointed sequence is eventually pointed in an infinite number of distinct ways with your current definition. Doing arithmetic on the modulus is surely useful, and for that you will need the untruncated version. This is analogous to the distinction between finite types and counting in univalent combinatorics. A finite type with $n$ elements has $n!$ distinct ways of being counted, but you don't for instance distinguish between two 2-element sets by the order in which the elements are counted.

[malarbol]

ok, what about has-modulus-eventually-pointed-sequence?

[fredrik-bakke]

This file can be called moduli-eventually-constant-sequences, leaving room for the eventual file (no pun intended)eventually-constant-sequences, which should consider the proof theoretically correct notion of eventually constant sequences.

[fredrik-bakke]

Please update the idea section to instead define moduli of eventually constant sequences

[fredrik-bakke]

Suggested change

	# Eventually constant sequences
	# Moduli of eventually constant sequences

[fredrik-bakke]

Suggested change

	### Eventually constant sequences
	### Moduli of eventually constant sequences

[fredrik-bakke]

Under your current definitions, you can't deduce that "an eventually constant sequence has a modulus" without a choice principle. By omitting the qualifier has you avoid this hairy problem with semantics. "Of course you can't extract a choice of a modulus from an eventually constant sequence without choice!"

Suggested change

	has-modulus-eventually-constant-sequence : UU l
	modulus-eventually-constant-sequence : UU l

This is analogous to how we say "countings of finite types" as opposed to "finite types have counting".

[fredrik-bakke]

I believe the standard nomenclature is to call this "eventual value" the "clustering point" or "asymptotic value". Please find a standard reference to follow for the terminology usage here.

[fredrik-bakke]

Suggested change

	### Constant sequences are eventually constant
	### Moduli of eventual constancy of constant sequences

[fredrik-bakke]

Suggested change

	### An eventually constant sequence is eventually equal to the constant sequence of its eventual value
	### A sequence with a modulus of eventual constancy has a modulus of eventual equality to the constant sequence of its ??asymptotic value??

[fredrik-bakke]

moduli-eventually-equal-sequences

[fredrik-bakke]

Please implement my suggestions for all of the contributed files

[malarbol]

Please implement my suggestions for all of the contributed files

Ok, I'll do my best. Do you have any suggestion for

• eventually equal --> modulus of eventual equality
• eventually constant --> modulus of eventual constancy
• eventually pointed --> ??

[malarbol]

I'll just stall this PR and go back to sequences in posets. Although it's really tempting to compare values "for sufficiently large n" I think I lack the experience to identify the good concepts, etc. For example, maybe the eventual stuff should be defined for sequences ℕ → Prop l?

[fredrik-bakke]

Moduli of eventually constant sequences, moduli of eventually equal sequences, moduli of eventually pointed sequences of types