From be1dff5b254387f228440312877cd43bb907bd19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 20 Nov 2023 15:55:01 +0100
Subject: [PATCH] Doc for sort poly inductives

---
 doc/changelog/01-kernel/17836-sort-poly.rst   |  1 +
 doc/sphinx/addendum/universe-polymorphism.rst | 53 +++++++++++++++++++
 2 files changed, 54 insertions(+)

diff --git a/doc/changelog/01-kernel/17836-sort-poly.rst b/doc/changelog/01-kernel/17836-sort-poly.rst
index d34ac26360ef0..94ad484cd9379 100644
--- a/doc/changelog/01-kernel/17836-sort-poly.rst
+++ b/doc/changelog/01-kernel/17836-sort-poly.rst
@@ -2,4 +2,5 @@
   :ref:`sort-polymorphism` makes it possible to share common constructs
   over `Type` `Prop` and `SProp`
   (`#17836 <https://github.com/coq/coq/pull/17836>`_,
+  `#18331 <https://github.com/coq/coq/pull/18331>`_,
   by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 8d791d02a918d..9355a33624f7e 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -803,6 +803,59 @@ witness these temporary variables.
    `α` followed by a number as printing will not distinguish between
    your bound variables and temporary variables.
 
+Sort polymorphic inductives may be declared when every instantiation
+is valid. Elimination at a given universe instance requires that
+elimination is allowed at every ground instantiation of the sort
+variables in the instance. These restrictions ignore
+:flag:`Definitional UIP`.
+
+For instance
+
+.. coqtop:: all reset
+
+   Set Universe Polymorphism.
+
+   Inductive Squash@{s|u|} (A:Type@{s|u}) : Prop := squash (_:A).
+
+Elimination to `Prop` and `SProp` is always allowed, so `Squash_ind`
+and `Squash_sind` are automatically defined.
+
+Elimination to `Type` is not allowed with variable `s`, because the
+instantiation `s := Type` does not allow elimination to `Type`.
+
+However elimination to `Type` or to a polymorphic sort with `s := Prop` is allowed:
+
+.. coqtop:: all
+
+   Definition Squash_Prop_rect A (P:Squash@{Prop|_} A -> Type)
+     (H:forall x, P (squash _ x))
+     : forall s, P s
+     := fun s => match s with squash _ x => H x end.
+
+   Definition Squash_Prop_srect@{s|u +|} A (P:Squash@{Prop|_} A -> Type@{s|u})
+     (H:forall x, P (squash _ x))
+     : forall s, P s
+     := fun s => match s with squash _ x => H x end.
+
+.. note::
+
+   Since inductive types in `SProp` with one or more constructors have
+   elimination restricted to `SProp`, inductive types in a polymorphic
+   sort have the same restriction. Additionally for uniformity of the
+   implementation this restriction is not removed by setting
+   :flag:`Definitional UIP`.
+
+   Consequently sort polymorphic containers such as sigma types are
+   better defined as primitive records (which do not have this
+   restriction) when possible.
+
+   .. coqtop:: all
+
+      Set Primitive Projections.
+      Record sigma@{s|u v|} (A:Type@{s|u}) (B:A -> Type@{s|v})
+        : Type@{s|max(u,v)}
+        := pair { pr1 : A; pr2 : B Rpr1 }.
+
 .. _universe-polymorphism-in-sections:
 
 Universe polymorphism and sections