Clean up the universal property of the integers

[VojtechStep]

I tried renaming elim-ℤ to ind-ℤ, but it turns out that that's already defined in elementary-number-theory.integers. The existing one isn't marked abstract, so it computes definitionaly and doesn't need the computation rules. Also there seems to be some overlap between elementary-number-theory.universal-property-integers and structured-types.initial-pointed-type-equipped-with-automorphism:

universal-property-integers	initial-pointed-type-equipped-with-automorphism
ELIM-ℤ'	hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut
universal-property-ℤ	is-initial-ℤ-Pointed-Type-With-Aut

The former proves the dependent universal property of the integers, and then shows the non-dependent one as a special case, while the latter builds just the theory of the non-dependent universal property (again, without referencing the other module). I'm not really sure how to proceed here.

As for the other renamings, I agree that there is some work to be done, but it's not so straightforward to adapt the conventions from dependent pushouts/the circle, because those constructions are somewhat dual; pushouts/the circle have an explicit evaluation map (dependent-cocone-map/ev-free-loop-Π) into data with characterized equality (htpy-dependent-cocone/Eq-free-dependent-loop), then show that it's an equivalence (dependent-universal-property-{pushout,circle}), and then deduce that the type of maps evaluating to the given data is contractible (uniqueness-dependent-universal-property-{pushout,circle}). They also call induction-principle-{pushout,circle} the fact that the evaluation map has a section. The integers go in the other direction: they have an explicit induction map (elim-ℤ) which produces a function from output data, then characterize structure preservation for the function (ELIM-ℤ), improve induction to produce proofs of structure preservation (Elim-ℤ), characterize equality of structure preserving maps (Eq-ELIM-ℤ), and show that the type of structure preserving maps producing the correct data is contractible (is-contr-ELIM-ℤ).

Written down like this, it seems to me like the construction is basically the same, except all of the definitions/constructions are for the "wrong" side of the equivalence 😅.

If we wanted to be consistent about what the names mean, I would suggest:

• Replacing elim-ℤ with ind-ℤ (but I'm not sure where to put it)
• Adding dependent-universal-property-ℤ : forall P -> is-equiv (\ (p0 , pS) -> Elim-ℤ p0 pS)
• Renaming is-contr-ELIM-ℤ -> uniqueness-dependent-universal-property-ℤ
• Renaming ELIM-ℤ -> structure-preserving-dependent-map-ℤ (analogue to structure-preserving-map-ℕ from elementary-number-theory.universal-property-natural-numbers)
• Renaming Elim-ℤ to either function-induction-principle-ℤ (mirroring function-induction-principle-circle) or ind-induction-principle-ℤ (mirroring ind-induction-principle-pushout); I prefer function-
• I'm not sure what the statement of induction-principle-ℤ would be in this case

Originally posted by @VojtechStep in #709 (comment)

At least we should do the renaming. It was later suggested to rename elim-ℤ to map-induction-principle-ℤ and Elim-ℤ to induction-principle-ℤ. It would be nice if we could go through the module structured-types.initial-pointed-type-equipped-with-automorphism, see if there are any redundancies, and if so then remove them.

@fredrik-bakke I think this is a good first issue, would you mind adding it the label?