Dedekind finiteness of various notions of finite type

[fredrik-bakke]

Defines

• Subfinite types
• Subfinitely indexed types
• Dedekind finite types
• dual Dedekind finite types
• Noninjective maps (maps for which there exists a repetition of values)

Proves

• Subfinite types are Dedekind finite
• Subfinitely indexed types are Dedekind finite
• Dedekind finite types validate the Cantor–Schröder–Bernstein theorem constructively
• finite choice under the double negation modality
• factor property of connected maps

+lost of small refactoring work

Resolves #748