proof assistant developers

Abstract: Diaconescu's theorem derives excluded middle from the axiom of choice, using propositional extensionality. We show that in dependent type theory without propositional extensionality, global choice alone does not imply excluded middle. We consider extensional Martin-Löf type theory with an impredicative universe of propositions included in the universe of types, extended with a global choice operator. We construct a consistent model of this type theory and show that the model refutes excluded middle and propositional extensionality. The model is built from staged sets, sets whose elements appear at stages of a well-order. It further validates proof irrelevance, inductive families, quotients with soundness, and a cumulative hierarchy of universes, which together cover a large fragment of the type theory of the proof assistant Lean. Even together with these features, global choice does not imply excluded middle.

Abstract: We explain an attempt to define semi-simplicial types (SST) in homotopy type theory by first defining a small type theory whose contexts are exactly the data of semi-simplicial types, constructing $\mathrm{SST}\,n$ uniformly in that syntax, and then interpreting the syntax in the universe. The syntax can be defined without any truncation and without K, and the construction of $\mathrm{SST}\,n$ goes through. The naive interpretation does not: it transports along the semantic images of equations that hold only propositionally, and making these transports agree needs uniqueness of identity proofs (UIP) for the semantic types. Moving the problem into the syntax, by making composition a constructor of a higher inductive-inductive type (HIIT), does not remove it either: it reappears as a coherence problem in the syntax. Fording the HIIT (storing equations instead of computed indices), with conditional rules, makes the syntax provably a set. This is UIP for the syntax, obtained by encode-decode, and it does not by itself restrict the semantics; but the naive interpretation of the conditional rules again needs UIP for the semantic types. A semantics into groupoids that avoids UIP will be discussed in a separate note. The Agda development accompanying this note is in the repository https://github.com/txa/sst-new.

Abstract: We present a dependently typed pure type system that contains a circular axiom $s : s$ for a certain sort $s$ and is nonetheless strongly normalizing. Girard's paradox is avoided because our sorts are not closed under a $Π$-former: function types are placed in sorts according to their rank. Turns out that this system has a unique set of characteristics: it has similar normalization behaviour as STLC (so complexity of normalization is TOWER-complete) while at the same time allowing non-uniform representation of arbitrary elementary recursive functions; furthermore, it has a nontrivial set-theoretical model in ZF+GCH and allows to carry out nontrivial proof developments. Base normalization proof is surprisingly simple (modulo general metatheoretical properties of pure type systems) and has been fully formalized in vanilla Rocq (formerly Coq) without additional axioms.

Abstract: In a type theory with a cumulative universe hierarchy, \emph{subtyping} is often incorporated to lift lower universe levels to higher ones. In practice, kernels of proof assistants typically implement universe subtyping conservatively: subtyping only propagates covariantly into the output types of $Π$ types, while input types must be equivalent. A full-blown subtyping relation also compares the input types contravariantly. However, contravariant subtyping is not justified by the existing set-theoretic model, and poses challenges in the development of a complete subtyping algorithm. We present \mclttsub, a complete mechanized study of contravariant universe subtyping for a core Martin-Löf type theory (MLTT), built as an extension of the verified McTT kernel in Rocq. We re-establish the syntactic meta-theory and the soundness and completeness properties of the normalization-by-evaluation (NbE) algorithm. To complete the verified pipeline for a type-checker, we give two complete and sound subtyping algorithms. The first one \emph{renormalizes} output types in every $Π$ iteration. Despite a simple completeness proof, this algorithm incurs additional computational cost. The second algorithm hence circumvents this cost by avoiding the renormalization at all. It simply recursively compares two already normalized types structurally. Nevertheless, a completeness proof of this algorithm in a semantic approach requires to reason about normalization in sub-contexts, a capability beyond what the current semantic gadget offers. Instead, we conduct a program equivalence proof through bisimulation relations. Using this technique, we prove that the NbE algorithm returns equal normal forms in sub-contexts up to universe levels, and successfully conclude the completeness of the subtyping algorithm.

Abstract: The Lean proof assistant has a rich library of mathematical formalizations that are interesting to users of other proof assistants. To help with the translation of this library to other systems, we present a theory in the Dedukti logical framework in which one can encode Lean terms and types, and define a typability-preserving translation from some large subset of Lean to that Dedukti theory.

Abstract: The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of $\mathrm{ZF}$. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of $\mathrm{ZF}$, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some $V_ρ$ is already a model of $\mathrm{ZF}$; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way $\mathrm{ZF}$ has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.

Abstract: We present a typed two-dimensional $λ$-calculus whose equality evidence is \emph{computational}: a path between two terms is an explicit finite sequence of one-step conversions (the $β$- and $η$-contractions, the congruences, and the structural rules), and every property of paths is proved \emph{by recursion over that sequence}, with any step as a base case --- in deliberate contrast with Martin-Löf type theory, where identity is generated by reflexivity alone and all properties go through the non-computational $J$-eliminator. The higher structure is imported from the $2β$- and $2η$-conversions of the theory of an arbitrary higher $λ$-model: we obtain 2-dimensional coherence laws, computable naturality of homotopies (via inductive homotopies and their explicit evaluations), a 2-dimensional path type with transport, and a parity invariant that proves the system consistent and \emph{really intensional}: the $β$- and $η$-contractions are provably distinct evidence, while in the native syntax of Idris (core MLTT) they are identified by definitional equality. Commutative diagrams accompany the main constructions, and the theory is fully formalized in Idris 2. A parallel Lean formalization is published in the Palomar registry \cite{palomar2026lean}. A philosophical reading closes the paper: constructivism in the BHK sense, proof-relevant intensionality, and the boundary between syntax and semantics, drawn relative to MLTT and HoTT.}