37
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      The identity type weak factorisation system

      Preprint
      ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.

          Related collections

          Most cited references11

          • Record: found
          • Abstract: not found
          • Article: not found

          FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES

          F. Lawvere (1963)
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Two-dimensional monad theory

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Generalised algebraic theories and contextual categories

                Bookmark

                Author and article information

                Journal
                2008-03-31
                2008-09-01
                Article
                10.1016/j.tcs.2008.08.030
                0803.4349
                02277449-ecda-4828-bc70-5b6bbc61cc76

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                03B15; 18C50; 18B40
                Theoretical Computer Science 409 (2008), no. 1, 94--109
                25 pages; accepted for publication in Theoretical Computer Science
                math.LO math.CT

                General mathematics,Logic & Foundation
                General mathematics, Logic & Foundation

                Comments

                Comment on this article

                scite_
                0
                0
                0
                0
                Smart Citations
                0
                0
                0
                0
                Citing PublicationsSupportingMentioningContrasting
                View Citations

                See how this article has been cited at scite.ai

                scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

                Similar content221

                Cited by18

                Most referenced authors33