pith. sign in

arxiv: 1010.1810 · v1 · pith:P7A4S3EXnew · submitted 2010-10-09 · 🧮 math.CT · math.LO

Type theory and homotopy

Steve Awodey This is my paper
classification 🧮 math.CT math.LO
keywords theoryhomotopytypealgebraarticlecategoriescomeconnection
0
0 comments X
read the original abstract

The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Martin-L\"of into homotopy theory, resulting in new examples of higher-dimensional categories.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

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

  1. Brave new categorical spectral positive Schubert geometry and the categorical Dual Amplituhedron

    math.CT 2026-06 unverdicted novelty 5.0

    The dissertation rewrites positive Schubert geometry via spectral algebraic geometry and differential cohesion to construct a categorical dual to the Amplituhedron with a De Rham volume.