natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Background
Basic concepts
equivalences in/of $(\infty,1)$-categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
In homotopy type theory, types represent $\infty$-groupoids, so there should be something similar to enriched $\infty$-groupoids in homotopy type theory. The following definition is an experimental definition of such an object:
Let $C$ be the subtype of types in a type universe $\mathcal{U}$ which satisfy a certain predicate $P$: for all types $T:C$, there is a term $p:P(T)$.
Then a type $T$ is $C$-enriched if for all terms $a:T$ and $b:T$, there is a dependent term $p(a,b):P(a = b)$, where $a = b$ is the identity type of $a$ and $b$ in $T$.
One could define $Ab$-enriched types, which are types whose identity types are all abelian groups (usually defined with a predicate $isAbelianGroup$).
Similarly, sets are $Prop$-enriched types, and $n$-types are $(n - 1)$Type-enriched types.
A (extended) lower Dedekind cut could be defined as a set $U:\mathcal{U}$ with an injection $i:U \hookrightarrow \mathbb{Q}$ which satisfy certain axioms, which are detailed in the article on Dedekind cuts. Then, one could define a (extended) Richman premetric space as a type whose identity types are (extended) lower Dedekind cuts, which in classical mathematics is the same as a (extended) metric space.
Under the relation between type theory and category theory, enriched types should correspond to enriched $\infty$-groupoids in higher category theory.
Last revised on June 16, 2022 at 11:25:59. See the history of this page for a list of all contributions to it.