Some closure properties of decidable maps and embeddings

[fredrik-bakke]

Formalizes a series of basic closure properties for decidable maps and embeddings.

• Left cancellation for decidable maps and embeddings
• Triangle properties for decidable maps and embeddings
• Σ-closure properties for decidable maps and embeddings
• Base change closure for decidable maps and embeddings
• Retract closure for decidable maps and embeddings
• Product closure for decidable maps and embeddings
• Coproduct closure for decidable maps and embeddings
• Factor out lemmas about decidable maps from decidable embeddings file

[EgbertRijke]

Looks great!