Logic, equality, and compactness

[fredrik-bakke]

A lot of results in logic and foundations.

Summary

• Types with decidable Σ-, Π-, and ∀-types
• Logical properties of maps
  • Irrefutably surjective maps
  • Propositionally double negation eliminating types
  • Propositionally decidable maps
  • Propositionally double negation eliminating maps
  • Hilbert $\varepsilon$-operators on maps
  • Double negation image
• Double negation dense equality and applications to decidability search
• Propositionally decidable types
• Infrastructure for logical properties on equality
  • Apartness relations
  • Tight apartness relations
  • Decidable equality
  • Double negation stable equality
  • Equality in decidable posets
• Structures on the booleans
• Increasing binary sequences
  • The type of increasing binary sequences
  • Inequality on increasing binary sequences
  • Bounded increasing binary sequences
  • Decidability search on increasing binary sequences
• Dirk Gently's principle
• Miscellaneous edits

[fredrik-bakke]

Martín just explained to me that the "types with double negation dense equality have decidable sigmas" result is a special case of "types are compact iff their totally separated reflections are compact", so that should be remarked in the appropriate places before merging.

[fredrik-bakke]

I'm going to do a self-review on this one in line with the discussed guidelines for self-review and then merge it so I can move on with my life.