Logic, equality, and compactness

[fredrik-bakke]

A lot of results in logic and foundations.

Summary

• Universal and existential decidability search (untruncated compactness)
• 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
• Infrastructure for logical properties on equality
  • Apartness relations
  • Tight apartness relations
  • Decidable equality
  • Double negation stable equality
  • Equality in decidable posets
• $\pi_0$-triviality, irrefutable $\pi_0$-triviality, and applications to compactness
• Propositionally decidable types
• Structures on the booleans
• The type of increasing binary sequences
• Dirk Gently's principle
• Indiscrete types
• Miscellaneous small edits