Subsingleton elimination and impredicativity for SProp, Prop and hProp

text/subsingleton-elimination.md

@@ -0,0 +1,176 @@
+- Title: Extended subsingleton elimination and subsingleton impredicativity, the case of `SProp`, `Prop` and `hProp`
+
+- Driver: Hugo Herbelin
+
+- Status: Draft
+
+-----
+
+# Bibliography
+
+  - [Definitional Proof-Irrelevance without K](https://hal.inria.fr/hal-01859964v2/document), Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
+  - This [Coq-club thread](https://sympa.inria.fr/sympa/arc/coq-club/2021-02/msg00092.html) on HoTT support
+
+# Summary
+
+The declaration of an inductive type in `SProp` and `Prop` can be seen as a truncation with respect to classes of formulas which we shall respectively call `SProp` and `Prop`.
+
+These classes are superset defined by syntactic criteria:
+- for `SProp`, as described in "Definitional Proof-Irrelevance without K":
+  - inductive types with at most one constructor whose components are recursively in `SProp` (section 3 of the paper), otherwise said inductive types generated by:
+    - `False`
+    - `True`
+    - any type previously declared in `SProp`
+    - any sigma-type of such types (without recursivity nor indices)
+  - inductive types with disjoint indices (sections 5 and 6 of the paper), a priori to be taken in small types, i.e. hsets
+- for actual `SProp`, as implemented in Coq 8.12:
+  - only the empty inductive type (possibly with indices)
+- for `Prop`: inductive types possibly with indices with at most one possibly-recursive constructor whose components are recursively in `Prop`, otherwise said inductive types generated by:
+    - `False`
+    - `True`
+    - any type previously declared in `Prop` (e.g. `ex A P`)
+    - any sigma-type of such types, as in `and`, possibly recursive as in `Acc`, possibly with indices as in `eq`. 
+
+These truncations are automatically considered as eliminable when the truncated type is syntactically recognized as belonging to the class (so-called "singleton elimination", which we could more accurately call "subsingleton elimination").
+
+The classes `Prop` and `SProp` are impredicative, in the sense that a dependent product of codomain `Prop` or `SProp` is again in the class.
+
+This CEPS is about three distinct extensions:
+- extending the definition of `Prop` and `SProp` classes with new syntactically decidable criteria
+- extending the dynamic detection of subsingleton elimination
+- adding a new class `HProp` providing an impredicative universe of subsingleton types; this extra `HProp` class would provide a variant of HoTT with impredicative `hProp` (`hProp := { A:Type & forall x y:A, x = y }`), alternative to using an axiom of resizing
+
+# Details of the current situation
+
+We review the current situation for `Prop` and `SProp`.
+
+## `Prop`
+
+Sort-polymorphism makes that inductive types are syntactically recognized in `Prop` after instantiation of parameters. For instance, `prod True True` is recognized as impredicative after instantiation:
+```
+Check Type -> prod True True.
+(* Type -> True * True
+     : Prop *)
+```
+Similarly in contexts where a `Prop` is expected:
+```
+Check and (prod True True) True
+(* True * True /\ True
+     : Prop *)
+```
+Contrastingly, subsingleton elimination is not recomputed dynamically:
+```
+Inductive PROD A B : Prop := PAIR : A -> B -> PROD A B.
+Check fun x : PROD True True => match x with PAIR _ _ _ _ => 0 end.
+(* Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set *)
+```
+which would actually be easy to address (see item 3 of the next section).
+
+## Actual `SProp`
+
+Actual `SProp` has no template polymorphism. Its subsingleton elimination is restricted to `False` so that dynamic computation of subsingleton elimination does not matter.
+
+We do not recommend template polymorphism for `SProp` (since template polymorphism is already planned to be superseded with universe polymorphism).
+
+In particular, we do not plan late detection of a parametric type in `Type` as an `SProp, nor late detection of a parametric type in `SProp` as supporting subsingleton type.
+
+# Detailed design for the `Prop` and `SProp` extensions
+
+## Uniformizing the treatment between `Prop` and `SProp`
+
+1. accept singleton types with all arguments in `SProp` to be in `SProp` as it is the case for `Prop`, the only difference being that recursive arguments are excluded; the indices should be in small types (i.e. `Prop` or `Set`)
+
+## Generalize the syntactic criterion for being in `Prop` or `SProp`
+
+2. accept in `SProp` and `Prop` singleton types with arguments of the form `forall a:A, B` when `B` is recursively an `SProp` or `Prop`-subsingleton
+3. accept in `SProp` and `Prop` types with several constructors when (small) indices justify that the constructors are disjoint (section 5 of "Definitional Proof-Irrelevance without K")
+
+## Dynamically recognizing subsingleton elimination for `Prop` and `SProp` in `match`
+
+4. This would require calling the subsingleton elimination checker dynamically when typing `match`.
+
+# Detailed design for the `HProp` addition
+
+Belonging to `HProp` is not decidable, so exactly characterizing `HProp` requires user-provided data.
+
+There are two solutions:
+- either we retarget `Prop` to include `HProp` (simpler)
+- or we keep `Prop` as it is and add a new subuniverse `HProp` (less change of habits)
+
+Both solutions follow the same way. Below, we assume the latter. To get the former, just use `Prop` instead of `HProp`.
+
+We shall avoid relying on template polymorphism. However, we may consider a `cast` of the form:
+```
+(t : HProp by p)
+```
+which forces the type-checker to recognize a type as being in a smaller universe than decidably detectable.
+
+The status of casts in the implementation is however fragile, so this may require some clarification of casts first.
+
+## New command to support arbitrary `HProp`
+
+We propose a new command:
+```
+Subsingleton id context : ishProp A := proof.
+```
+which recast the type of `A` from `context -> Type` to `context -> HProp` so that it is latter considered impredicative.
+
+An alternative is to have a modifier to definitions in the form:
+```
+Subsingleton id context := def : HProp by proof.
+```
+But then, we probably want also:
+```
+Subsingleton id context := def : Hprop.
+Proof.
+the proof of being hProp
+Qed.
+```
+which may be complicated.
+
+If `HProp` is made distinct from `Prop`, new declarations `Inductive ... : ... -> HProp` would be accepted too. When to tell that the type has subsingleton elimination? There is a proposal in the next section.
+
+## Dynamic detection of subsingleton elimination
+
+We propose an extension of `match` of the following form:
+```
+match t as id in I params return typ by u with
+| C1 vars => body
+...
+| Cn vars => body
+end
+```
+where, when `I` is `HProp`-truncated but the instance `I args` is an `HProp` proved by `u : forall x y:I args, x = y`, the elimination to `Type` is allowed.
+
+# Side remark on template polymorphism for `Prop`
+
+Instances of parametric types which are not in `Prop` in the general case are automatically recognized as belonging to the `Prop` class (and treated as subsingleton for `match` and as impredicative in function types) when the parameters are themselves in `Prop`. This is typically the case of `prod A B` which behaves as `and A B` when `A` and `B` are in `Prop`.
+
+Template polymorphism induces a view where an inductive type in `Prop` does not necessarily mean explicitly `Prop`-truncated. It is so only when the original type is not a syntactic `Prop`-subsingleton.
+
+Without template polymorphism, explicit coercions from `prod A B` to `and A B` should be inserted (when `A` and `B` are `Prop`), and explicit Prop-boxing of `prod A B` should be done to make `prod A B` behave impredicatively.
+
+# Issues with extraction of `HProp`
+
+Types in `HProp` which are not in the current syntactic class `Prop` could simply be extracted as if they were types.
+
+# Conclusion
+
+A few extensions could be done pretty easily:
+1. accept singleton types with all arguments in `SProp` to be in `SProp` (`True`, `and`, ...)
+2. accept in `SProp` and `Prop` singleton types with arguments of the form `forall a:A, B` when `B` is recursively an `SProp` or `Prop`-subsingleton
+4. dynamically recognize subsingleton elimination for `Prop` and `SProp` in `match`
+
+The "disjoint indices" extension would require some days of work:
+
+4. accept in `SProp` and `Prop` types with several constructors when (small) indices justify that the constructors are disjoint (section 5 of "Definitional Proof-Irrelevance without K")
+
+The support for `HProp` distinct from `Prop` would require introducing the new subuniverse `HProp` at many places of the code and may be costly.
+
+However, scaling `Prop` to `HProp` would only require the new independent commands:
+
+5. `Subsingleton ...`
+6. `match ... by p with ... end`
+7. `(t : HProp by p)`
+
+and each of them are worth a design discussion.