How does Prop relate to h-prop and double negation?

Question

I'm referring to these concepts:

• Prop in Agda and SProp in Coq, a "sort of definitionally proof-irrelevant propositions", and their squash type (and relatedly, the usual Prop in Coq);
• mere propositions and propositional truncation in HoTT (see §3.7 of the book); and
• double negation.

These all clearly have some things in common, for example:

• axioms like LEM* and choice**,
• a modality (resp. squash, truncation, and double negation) which implies double negation (i.e. Squash A → ¬¬ A), and
• propositional truncation and double negation are classically equivalent, and the HoTT book says they have the same universal property, although I'm not sure what that means (related?).

There also appear to be some observable differences, for example:

• The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible.

• From comments and answers on my question on canonicity for irrelevant types:

  SProp terms are propositionally truncated, which means that no model can distinguish terms of the same SProp type.

  The funny thing with SProp is that it gives a generalization of the result that consistent negative axioms can be postulated without breaking canonicity.

  HoTT (with the UA as an axiom) also satisfies weak canonicity, in the sense that every term is propositionally equal to a canonical term.

• Substructural (e.g. paraconsistent and/or paracomplete) systems may have multiple forms of falsity and negation (for example 'implies bottom' or 'implies zero' in linear logic, or 'top excludes' from basic logic, and I don't know how or if these could be related. (Perhaps zero and bottom relate to proof-relevance for falsity? Zero and top have "kirby-reduction" and "katamari-expansion" eta rules which eat everything.)

How are these different truncation-like modalities and their respective propositions related? Additionally,

• How many constructively (or even substructurally) inequivalent truncation-like modalities are there?
• Do axioms for one imply axioms for the other? Could you even have different (or even mutually inconsistent) axioms for each?

* Double negation does not entirely get LEM as a theorem. You get ∀ {A : Set} → ¬¬ (¬ A + A) but not ¬¬ ∀ {A : Set} → (¬ A A) without double negation shift.

** e.g. (∀ (x : A) → Squash (P x)) → Squash (∀ (x : A) → P x)

Answer 1

You have a looot of questions. It's a bit hard to see how many are there, but let me write something that I believe to answer your questions.

• A type A is said to be hProp (HoTT mere propositions) if you can prove (x y : A) -> x = y (usually called isProp A) for the propositional equality type =, usually intensional. A function taking a hProp is written as (A : Type) -> (p : isProp A) -> .... So, hProp is usually just a conceptual thing, in type theory syntax we talk about isProp predicate.
  • Arend proposed a new design that makes hProp a universe, which IMO is a very good design (but requires builtin path type).
• A type is said to be a Prop (Agda Prop or Coq SProp) if the type theory considers all instances of A equal definitionally, and this is only by definition. You can't prove a type to be in Prop -- it's either defined in Prop or not in Prop at all. Prop is a type that exists in the syntax of type theory.
  • Prop is usually predicative, because impredicative Prop leads to loss of normalization (ref). Lean4 adapts this design.
• Double negation is just what it is, I think you understand it. It is not that equivalent to hProp -- classically equivalent means that classical axioms (like LEM/DNE) implies they're equivalent, so without these assumptions you can't say so.

You can either "truncate" a thing to Prop or hProp. For the former you define a Prop parameterized by a Type, and for the latter you use a higher inductive type (I assume you know what this is because you're reading hott book) or the lambda encoding of (h-)propositional truncation.