Pith. sign in

REVIEW 1 cited by

Morita equivalences between algebraic dependent type theories

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1804.05045 v2 pith:O4OBWZXC submitted 2018-04-13 math.CT cs.LOmath.LO

Valery Isaev This is my paper · ORCID
classification math.CTcs.LOmath.LO
keywords equivalencetheoriesmodelsmoritatypealgebraiccategorydependent
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We define a notion of equivalence between algebraic dependent type theories which we call Morita equivalence. This notion has a simple syntactic description and an equivalent description in terms of models of the theories. The category of models of a type theory often carries a natural structure of a model category. If this holds for the categories of models of two theories, then a map between them is a Morita equivalence if and only if the adjunction generated by it is a Quillen equivalence.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Extension Types for Free

    cs.LO 2026-07 accept novelty 8.0 of 10 full

    Extension types are definable in two-level type theory, all their Riehl–Shulman rules become theorems, and cubical gluing is equivalent to univalence in this framework.

Pith tools