Constructive Definitional Extensions and Morita Equivalence

Definitions and mathematical statement

The supplied question concerns theories and extensions of theories in an unspecified constructive logical framework. Its proposed extension operations are the addition of abbreviations, logical constructors, unique-existence terms, and standard sorts, including subsorts, quotient sorts, finite products, and finite disjoint unions. The phrase "such as" in the source does not specify whether this list of sorts is exhaustive.

A conditional formalization of the intended comparison is as follows. Fix a class $\mathcal T$ of theories in the intended constructive framework, and let $\mathcal A\subseteq\mathcal T\times\mathcal T$ be the relation of admissible extensions using the listed operations, once their precise admissibility conditions have been specified. Define the equivalence relation generated by these extensions by \[ \equiv_{\mathcal A} := \bigcap\{R\subseteq\mathcal T\times\mathcal T: R\text{ is an equivalence relation and }\mathcal A\subseteq R\}. \] Let $M\subseteq\mathcal T\times\mathcal T$ denote the intended relation of constructive Morita equivalence, whose definition must also be fixed. The question is whether \[ \forall S,T\in\mathcal T,\qquad S\equiv_{\mathcal A}T \quad\Longleftrightarrow\quad (S,T)\in M. \] This is a formulation schema, not a fully specified mathematical assertion: the source does not define $\mathcal T$, $\mathcal A$, or $M$. In particular, it does not specify the underlying constructive logic, the meaning of adding logical constructors, the hypotheses for introducing unique-existence terms or new sorts, or the intended notion of constructive Morita equivalence. The background describes related conservative-extension phenomena but gives no precise conservativity requirement. These missing choices must be recovered before the displayed comparison has a determinate meaning.

Short English statement

Does equivalence generated by the indicated constructive extensions of theories coincide with constructive Morita equivalence? The supplied record labels this question open, but its logical framework and both equivalence notions require clarification before a fully precise statement can be given.

Sources

• Local registry: data/unsolvedmath/problems.json, permanent UnsolvedMath ID $30004557$, source problem code catalogue entry; collection: Oberwolfach Reports Open Problems. The supplied record gives proposed year $2020$ and names no proposer.
• Supplied report citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2021), Oberwolfach Reports, DOI 10.4171/owr/2020/34, pp. 1693--1757. Supplied source URL and literature-source label "Oberwolfach Report 34/2020": https://doi.org/10.4171/owr/2020/34. The background describes Oberwolfach Reports as documenting mathematical workshops and their open-problem discussions. No pinpoint location for this question is supplied.
• Additional supplied literature source: "Rynasiewicz--Tsementzis, 2015", https://arxiv.org/abs/1507.02302. No title, pinpoint reference, or precise supporting result is supplied.
• Literature assessment dated exactly 2026-08-22: supplied dated curation, not independently verified. It labels the problem open and reports that the conservative-extension phenomena are related to Morita equivalence, while no result identified in that curation establishes the requested identification with constructive Morita equivalence. The background characterizes this assessment as dated literature triage derived from supplied OWR curation and requests independent verification of time-sensitive status and cited claims. Neither linked source has been independently consulted for this draft.