Pith. sign in

REVIEW 1 cited by

Modalities in homotopy type theory

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 1706.07526 v6 pith:CPF3L7JC submitted 2017-06-22 math.CT cs.LOmath.LO

Egbert Rijke , Michael Shulman , Bas Spitters This is my paper · ORCID
classification math.CTcs.LOmath.LO
keywords theorytypehomotopymodalitiesdevelopfactorizationhigherinternal
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
abstract

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.

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. Good Fibrations through the Modal Prism

    math.CT 2019-08 accept novelty 7.0 of 10

    A new notion of modal fibration is introduced and characterized by locally constant modal fibers, yielding new synthetic proofs of the fundamental group of the circle, Hopf fibrations, and covering space theory.

Pith tools