ch:cic: ch:cic

For the inner product $A\to \mathsf{Type}@\{v\}$, the domain has sort $\mathsf{Type}@\{u\}$ and the codomain term has sort $\mathsf{Type}@\{v+1\}$, so its sort is $\mathsf{Type}@\{max(u,v+1)\}$. The outer domain $\mathsf{Type}@\{u\}$ itself has sort $\mathsf{Type}@\{u+1\}$. Hence the whole product has sort $$\mathsf{Type}@\{max(u+1,v+1)\}.$$ Equivalently, a fresh result level $w$ needs the constraints $u+1\le w$ and $v+1\le w$. If the innermost codomain is $\mathsf{Prop}$, both products have propositional codomain; impredicativity makes their final sort $\mathsf{Prop}$ instead of taking a maximum.

At universe $u$, declare $$\mathsf{Tree}@\{u\}(A:\mathsf{Type}@\{u\}):\mathsf{Type}@\{u\},$$ with $\mathsf{leaf}:A\to \mathsf{Tree}(A)$ and $\mathsf{node}:\mathsf{Tree}(A)\to \mathsf{Tree}(A)\to \mathsf{Tree}(A)$. The sole parameter is $A$; there are no indices. Both recursive occurrences are constructor arguments in positive positions, and every conclusion uses the same parameter $A$. The judgment $\mathsf{Type}@\{u\}:\mathsf{Type}@\{u+1\}$ is sort formation, not a nontrivial declared universe constraint. This declaration can therefore have an empty constraint set. Choose its stored $\mathsf{ind}\mathsf{\_}\mathsf{kelim}$ list to be $[\mathsf{Prop},\mathsf{Set},\mathsf{Type}]$; the frozen 2019 $\mathsf{check}\mathsf{\_}\mathsf{ind}\mathsf{\_}\mathsf{sorts}$ does not validate that list for a Type-valued inductive. A field $\mathsf{Tree}(A)\to A$ moves the family to the domain of an arrow inside a constructor argument, so the positivity path fails at constructor-arg/domain.

Environment checking uses universe-graph validity and the graph and inductive-body obligations. Weak-head normalization uses normalization, subject reduction, strengthening, and stability of fix guards under the transformations performed during reduction. Conversion additionally uses proof irrelevance and the conversion metatheory. Type inference uses validity and principality to relate inferred and expected types. Declaration checking uses the positivity/fix or configuration guards and the checked environment interfaces. Confluence says that two reductions from one term can be joined; it neither proves that reduction terminates nor constructs a total weak-head-normalization function. The strong-normalization assumption is therefore not discharged by confluence.

For equality, a motive may be $$P_{=}:=\lambda y.\lambda e.A:\prod _{y:A}\mathsf{Eq}(A,x,y)\to \mathsf{Type}@\{u\}.$$ The reflexivity branch is the actual term $x:P_{=}(x,\mathsf{refl})$, so the equality case returns an element of $A$ and is admitted by the stored singleton-elimination information. For the existential, take the equally explicit Type-valued motive $$Q:=\lambda e.A:\mathsf{Exists}(A,R)\to \mathsf{Type}@\{u\},b:=\lambda x.\lambda p.x.$$ The proposed branch has type $\prod _{x:A}\prod _{p:R(x)}Q(\mathsf{intro}(x,p))$ and would return the hidden witness. It is rejected: the constructor field $x:A$ is an informative witness, so this propositional inductive is not in the singleton-elimination class. A $\mathsf{Prop}$-valued motive remains admissible.

Let $I_V:=(\mathit{kn},0)$ be the inductive identifier for the sole body of the vector mutual block, let $u$ be its universe instance, and let the constructor numbers be $0$ for nil and $1$ for cons. The three raw references are $$\begin{array}{c}\mathsf{Ind}(I_V,u),\\ \mathsf{Construct}(I_V,0,u),\\ \mathsf{Construct}(I_V,1,u).\end{array}$$ For $z:\mathsf{Ind}(I_V,u)An$, a dependent case predicate has type $$\prod _{m:\mathbb{N}}\mathsf{Ind}(I_V,u)Am\to \mathsf{Type}@\{w\}.$$ The case information is exactly $(I_V,1)$: there is one uniform parameter. Its raw branch list has arities $$[(0,b_{\mathsf{nil}}),(3,b_{\mathsf{cons}})].$$ The nil branch has type $P0(\mathsf{Construct}(I_V,0,u)A)$. The raw cons branch quantifies only $$m:\mathbb{N},x:A,xs:\mathsf{Ind}(I_V,u)Am$$ and returns $P(\mathsf{suc}m)(\mathsf{Construct}(I_V,1,u)Amxxs)$. The kernel case rule supplies no induction hypothesis. The separate generated induction constant has a cons method that additionally quantifies $ih:Pmxs$ before returning the same displayed result. Here $A$ is the uniform parameter, $m$ the index, $xs$ the recursive vector, and $ih$ the result of the induction fixpoint’s recursive call on $xs$.

Use $I_V=(\mathit{kn},0)$, case information $(I_V,1)$, and raw branches $[(0,b_0),(3,b_1)]$. The complete constructor-headed redex is $$\mathsf{Case}((I_V,1),P,\mathsf{apps}(\mathsf{Construct}(I_V,1,u),[A,m,x,xs]),[(0,b_0),(3,b_1)]).$$ By PCUIC-$\iota$ it reduces in one step to the literal substitution result $$\mathsf{apps}(b_1,\mathsf{skipn}(1,[A,m,x,xs]))\equiv \mathsf{apps}(b_1,[m,x,xs]).$$ No recursive call or induction hypothesis is inserted by this reduction.

For a projection $p$ and a block with $\mathsf{unfoldCoFix}(\overline{d},k)=(n_a,f)$, the complete raw step is $$\mathsf{Proj}(p,\mathsf{apps}(\mathsf{CoFix}(\overline{d},k),\overline{a})){⇝}_0\mathsf{Proj}(p,\mathsf{apps}(f,\overline{a})).$$ Projection from a constructor is a separate next step. For a fixpoint, $$\mathsf{apps}(\mathsf{Fix}(\overline{e},j),\overline{q}){⇝}_0\mathsf{apps}(g,\overline{q})$$ requires both $\mathsf{unfoldFix}(\overline{e},j)=(r,g)$ and $\mathsf{isConstructor}(r,\overline{q})=\mathsf{true}$. Replacing $\overline{q}[r]$ by the neutral $\mathsf{Rel}(0)$ makes the Boolean false, so this root rule has no derivation.

The generated vector induction constant places recursion in its fix body. In its cons branch the raw body has the form $$\lambda m.\lambda x.\lambda xs.\mathsf{apps}(s,[m,x,xs,\mathsf{apps}(\mathsf{Fix}(\overline{e},j),[m,xs])]).$$ Thus the explicit fix application on $xs$, not the kernel case branch arity, creates the induction hypothesis.

The frozen archive gives the following exact witnesses and gaps. Unqualified filenames below are under pcuic/theories/; other paths name their archive roots explicitly.

Confluence. PCUICConfluence.v completes red_confluence.

Subject reduction. PCUICSR.v admits sr_red1; subject_reduction is derived from that admitted environment property.

Validity, strengthening, principality, and normalization. pcuic/theories/PCUICValidity.v admits validity; pcuic/theories/PCUICSafeLemmata.v admits the declaration strengthening at line 1283 of the frozen file; pcuic/theories/PCUICPrincipality.v admits principal_typing; and pcuic/theories/PCUICSN.v declares normalisation as an axiom and admits normalisation’.

Proof irrelevance in graph equality. The comment immediately before graph_eq in template-coq/theories/common/uGraph.v marks its proof-irrelevance step; the lemma identifies canonical graph representations and is consumed by the safe checker.

Safe checker. safechecker/theories/PCUICSafeChecker.v admits check_one_ind_body, add_uctx_make_graph, gc_of_constraints_union, and no_prop_levels_union; it declares graph_eq as an axiom. Its typecheck_program definition has a dependent, squashed typing conclusion, so safe-checker soundness is conditional on this theory base. Checker completeness is separately open: pcuic/theories/PCUICCheckerCompleteness.v contains only its license header and no completeness declaration.

Erasure. erasure/theories/ErasureCorrectness.v proves erases_correct, relative to well-formed typing and weak call-by-value. Consequently canonicity and consistency remain open. The paper’s first-order erasure corollaries are explicitly nonmechanized and therefore occupy a separate status cell. No result from the living MetaRocq checkout changes any of these historical cells.