From 77d4c058261e6e843a4a80f7f0290c4798d0f5ec Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 16:31:04 +0200
Subject: Improve documentation of cumulativity

---
 doc/refman/Universes.tex | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 2bb1301c79..79b9e4df52 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -139,7 +139,9 @@ producing global universe constraints, one can use the
 Inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
 there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative. Consider the examples below.
+makes all subsequent inductive definitions cumulative.  When set
+inductive types and the like can be enforced to be
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
 Polymorphic Cumulative Inductive list {A : Type} :=
 | nil : list
@@ -176,6 +178,25 @@ Print packType.
 \end{coq_example}
 Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
 
+Cumulative inductive types, coninductive types, variants and records
+only make sense when they are universe polymorphic. Therefore, an
+error is issued whenever the user inputs such monomorphic and
+cumulative type. Notice that this also implies that when the option
+\texttt{Set Inductive Cumulativity} is set any subsequent inductive
+declaration should be polymorphic, e.g., by setting \texttt{Set
+  Universe Polymorphism}, unless it is specifically made
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix.
+
+\begin{coq_example}
+Fail Monomorphic Cumulative Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+Set Inductive Cumulativity.
+Fail Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+NonCumulative Inductive Unit := unit.
+\end{coq_example}
 
 \asection{Global and local universes}
 
-- 
cgit v1.2.3


From 28998d55aaaf0ad0e78477db5601a5bc9a6657b1 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 17:57:01 +0200
Subject: Fix typo and Add Jason's example to the doc

---
 doc/refman/Universes.tex | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 79b9e4df52..e097de59b3 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -139,7 +139,7 @@ producing global universe constraints, one can use the
 Inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
 there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative.  When set
+makes all subsequent inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
 \emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
@@ -180,7 +180,7 @@ Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
 
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
-error is issued whenever the user inputs such monomorphic and
+error is issued whenever the user inputs such a monomorphic and
 cumulative type. Notice that this also implies that when the option
 \texttt{Set Inductive Cumulativity} is set any subsequent inductive
 declaration should be polymorphic, e.g., by setting \texttt{Set
@@ -198,6 +198,29 @@ Fail Inductive Unit := unit.
 NonCumulative Inductive Unit := unit.
 \end{coq_example}
 
+\subsection*{An example of a proof using cumulativity}
+
+\begin{coq_example}
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B.
+  Proof.
+    exact H.
+  Defined.
+\end{coq_example}
+
 \asection{Global and local universes}
 
 Each universe is declared in a global or local environment before it can
-- 
cgit v1.2.3


From 819fd4a7a431efb41a080e7aabef2a66a3ca2417 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Mon, 31 Jul 2017 11:50:54 +0200
Subject: Update documentation of cumulativity

---
 doc/refman/Universes.tex | 45 ++++++++++++++++++++-------------------------
 1 file changed, 20 insertions(+), 25 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index e097de59b3..667fd66984 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -134,12 +134,12 @@ producing global universe constraints, one can use the
 \asection{{\tt Cumulative, NonCumulative}}
 \comindex{Cumulative}
 \comindex{NonCumulative}
-\optindex{Inductive Cumulativity}
+\optindex{Polymorphic Inductive Cumulativity}
 
-Inductive types, coinductive types, variants and records can be
+Polymorphic inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
-there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative.  When set,
+there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
+makes all subsequent \emph{polymorphic} inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
 \emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
@@ -160,15 +160,6 @@ This also means that any two instances of \texttt{list} are convertible:
 $\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
 furthermore their corresponding (when fully applied to convertible arguments) constructors.
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
-Also notice the subtyping constraints for the \emph{non-cumulative} version of list:
-\begin{coq_example*}
-Polymorphic NonCumulative Inductive list' {A : Type} :=
-| nil' : list'
-| cons' : A -> list' -> list'.
-\end{coq_example*}
-\begin{coq_example}
-Print list'.
-\end{coq_example}
 The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
 Polymorphic Cumulative Record packType := {pk : Type}.
@@ -176,33 +167,37 @@ Polymorphic Cumulative Record packType := {pk : Type}.
 \begin{coq_example}
 Print packType.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
+Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
+convertible if and only if \texttt{i $=$ j}.
 
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
-error is issued whenever the user inputs such a monomorphic and
-cumulative type. Notice that this also implies that when the option
-\texttt{Set Inductive Cumulativity} is set any subsequent inductive
-declaration should be polymorphic, e.g., by setting \texttt{Set
-  Universe Polymorphism}, unless it is specifically made
-\emph{non-cumulative} using the \texttt{NonCumulative} prefix.
-
+error is issued whenever the user uses the \texttt{Cumulative} or
+\texttt{NonCumulative} prefix in a monomorphic contexts.
+Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}.
+That is, this optiotion, when set, makes all subsequent \emph{polymorphic}
+inductive declarations cumulative (unless, of course if the \texttt{NonCumulative} prefix is used)
+but has no effect on \emph{monomorphic} inductive declarations.
+Consider the following examples.
 \begin{coq_example}
 Fail Monomorphic Cumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example}
-Set Inductive Cumulativity.
-Fail Inductive Unit := unit.
+Fail Monomorphic NonCumulative Inductive Unit := unit.
 \end{coq_example}
+\begin{coq_example*}
+Set Polymorphic Inductive Cumulativity.
+Inductive Unit := unit.
+\end{coq_example*}
 \begin{coq_example}
-NonCumulative Inductive Unit := unit.
+Print Unit.
 \end{coq_example}
 
 \subsection*{An example of a proof using cumulativity}
 
 \begin{coq_example}
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 
 Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
 
-- 
cgit v1.2.3


From 2f0e71c7e25eb193f252b6848dadff771dbc270d Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 2 Aug 2017 09:42:37 +0200
Subject: Typo in the documentation of cumulativity

---
 doc/refman/Universes.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 667fd66984..cd36d1d320 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -173,17 +173,17 @@ convertible if and only if \texttt{i $=$ j}.
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the \texttt{Cumulative} or
-\texttt{NonCumulative} prefix in a monomorphic contexts.
+\texttt{NonCumulative} prefix in a monomorphic context.
 Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}.
-That is, this optiotion, when set, makes all subsequent \emph{polymorphic}
-inductive declarations cumulative (unless, of course if the \texttt{NonCumulative} prefix is used)
+That is, this option, when set, makes all subsequent \emph{polymorphic}
+inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used)
 but has no effect on \emph{monomorphic} inductive declarations.
 Consider the following examples.
 \begin{coq_example}
-Fail Monomorphic Cumulative Inductive Unit := unit.
+Monomorphic Cumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example}
-Fail Monomorphic NonCumulative Inductive Unit := unit.
+Monomorphic NonCumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example*}
 Set Polymorphic Inductive Cumulativity.
-- 
cgit v1.2.3