Propositional operations

[fredrik-bakke]

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.

[EgbertRijke]

I think in most cases where we use infix notation I would still like to keep a regular name, and not dispose of it. The regular name for the operation then sets the naming scheme for things involving that operator, because generally we don't use unicode symbols in the middle of a name.

Also, the sentence from your PR description

The suggested scheme is to use unicode symbols when taking values in types, and spelled-out words when taking values in types.

should probably mention propositions in one of the two cases.

[fredrik-bakke]

Also, the sentence from your PR description

The suggested scheme is to use unicode symbols when taking values in types, and spelled-out words when taking values in types.

should probably mention propositions in one of the two cases.

Ah, thanks for spotting that. I fixed it now.

To be clear, I'm not too fond of the current proposed scheme. I don't like _and_, _or_, _iff_, or _implies_ because

1. they add extra names to things that already have names, and it is not at all clear for a person who is not already familiar with them what their relation is to the unicode operators.
2. They go against our conventions.
3. They look too much like arguments to functions when writing things like P iff Q. (This can be remedied somewhat by writing (P) iff (Q))

However, I also don't like how we have to write type-conjunction-Prop, type-disjunction-Prop, type-iff-Prop and type-hom-Prop for them otherwise. Maybe it is better to prefer using the unicode operators and then wrapping the final expression in a type-Prop. Alternatively, we could also consider having definitions of the form conjunction : Prop -> Prop -> UU, iff : Prop -> Prop -> UU and so on (not infix operators).

[fredrik-bakke]

It seems to me the questions that remain open are

• What do we do with ∃?

and

• should we have another operator for negation on propositions?

Other than this, I do like the prospect of having a "DSL" for propositions.

[fredrik-bakke]

I am tempted to give up on the current draft again, as I don't believe the notation ∨₍₋₁₎ etc. does very much to help readability in the end. It just adds yet another way to say the same thing. I think that is too bad, but perhaps the best way to work with propositions is to take _∨_ to mean the propositional disjunction type of types and similarly _∧_ to mean the underlying type of the propositional conjunction on types (this will require a slight refactoring of the current file). That does leave _⇒_ and _⇔_ in a slightly awkward position though. Should they also be the propositional truncation of maps and logical equivalences respectively?

[EgbertRijke]

I'm only at 83/193 files reviewed. Sorry once again for the slow process.