Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Small refactorings for real numbers #1060

Open
3 tasks
fredrik-bakke opened this issue Mar 7, 2024 · 0 comments
Open
3 tasks

Small refactorings for real numbers #1060

fredrik-bakke opened this issue Mar 7, 2024 · 0 comments

Comments

@fredrik-bakke
Copy link
Collaborator

Real numbers

  • Factor out lower and upper Dedekind cuts into their own files.
  • lower and upper Dedekind reals should probably be their own files too.
  • Use the theory of lower and upper sets of posets in the definition of Dedekind cuts.
EgbertRijke added a commit that referenced this issue Apr 11, 2024
## Summary
- Introduce a general naming scheme for infix endooperations on
propositions and the corresponding endooperations on types
- Remove uses of `∀`
- remove the redundant `implication-Prop`
- Add table for propositional logic
- Add table for operations on propositions
- Correct the definition of exclusive disjunction. It is now named
"exclusive sum" (up for discussion)
- Introduce _disjunction_, (the correct definition of) _exclusive
disjunction_, and _mere logical equivalence_ of types
- Introduce _coinhabitedness_ of types
- Introduce universal quantification
- Define the homotopy preorder of types
- Prove that existential quantification of type families agrees with
existential quantification of the propositional reflection of the type
family
- Prove that disjunction of types agree with disjunction of the
propositional reflections of the summands

Intersects with #1060.
Resolves #984.

---------

Co-authored-by: Egbert Rijke <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant