9
$\begingroup$

I'm referring to these concepts:

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)

$\endgroup$
1
  • $\begingroup$ Sorry if this question is somewhat broad, vague, or hard to answer. I've been sitting on it for a few weeks hoping I'd come up with a better way to formulate it, but never did. I was prompted to finally ask it after talking with Paraconsista and MBones asked a very similar question. If you think you can improve the question, please edit away. $\endgroup$ Mar 25 at 19:20

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ The problem is I understand what they are, but I don't know concretely what you could or could not prove using one but not the other. More generally they seem to encompass some sort of idea of "proposition-like" or "truncation-like" but I don't know if there's actually a concrete idea relating them. $\endgroup$ Mar 25 at 19:52
  • $\begingroup$ Also, the intended question is "How are these different truncation-like modalities and their respective propositions related?". I elaborate on it with two specific examples of what "related" might mean. Any other question marks or "not sure" is speculation which I was hoping would clarify why I feel like "truncation-like" could make sense as a concept (to hope that they're unified in some way), but if they just add confusion about the question they should be edited out. $\endgroup$ Mar 25 at 19:54
  • $\begingroup$ Based on that I'm not sure if the question is answerable as written, so it may need to be closed if that's the case. It might be one of those questions that you don't know how to ask until you already know the answer. $\endgroup$ Mar 25 at 19:59
  • 2
    $\begingroup$ Impredicative SProp breaks SN only when you can eliminate the SProp equality into a non-SProp sort. Otherwise, it's fine. $\endgroup$ Mar 27 at 16:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.