under construction
In Shulman18, the authors write
One might argue that it would be better to include a separate kind of type representing objects in the base category, and type constructors represent-ing the functors $p_*$, $p^*$, etc. rather than the monads and comonads they induce. This would be in line with the “judgmental deconstruction” of Reed (2009) that decomposes $\Box$ and $\bigcirc$ into pairs of adjoint functors. It could be that this is indeed better; in fact, the current rules for $\flat$ and $\sharp$ were deduced from a generalization of Reed (2009) developed by Licata and Shulman (2016).
This is an attempt at developing such a cohesive homotopy type theory.
This presentation of cohesive homotopy type theory is a dependent type theory consisting of two different kinds of types, spaces and homotopy types. There exist judgments
for spaces
for homotopy types
for points
for terms
for fibrations
for dependent types
for sections
for dependent terms
Cohesive homotopy type theory has the following additional judgments, 2 for turning spaces into homotopy types and the other two for turning homotopy types into spaces:
Every space has an underlying homotopy type
Every space has a fundamental homotopy type
Every homotopy type has a discrete space
Every homotopy type has an indiscrete space
The underlying homotopy type and fundamental homotopy type are sometimes represented by the greek letters $\Gamma$ and $\Pi$ respectively, but both are already used in dependent type theory to represent the context and the dependent product type.
From these judgements one could construct the sharp modality as
the flat modality as
and the shape modality as
for a space $S$.
The fundamental homotopy type of the unit space is equivalent to the unit type.
The product of the fundamental homotopy types of spaces $A$ and $B$ is equivalent to the fundamental homotopy type of the product of spaces $A$ and $B$:
Created on June 19, 2022 at 23:30:27. See the history of this page for a list of all contributions to it.