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
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
(2,1)-quasitopos?
structures in a cohesive (∞,1)-topos
As geometric type theory refers to a conjectural extension of geometric logic to an extensional dependent type theory that corresponds to sheaf toposes (under the relation between category theory and type theory) with geometric morphisms between them, a similar conjectural extension to a homotopy type theory corresponding to (∞,1)-sheaf (∞,1)-toposes (and geometric morphisms) maybe deserves to be called geometric homotopy type theory.
Since homotopy colimits are preserved by inverse images of geometric morphisms, this type theory is likely to include at least non-recursive higher inductive types, and furthermore perhaps free models for every (finite) essentially algebraic (infinity,1)-theory. (Arbitrary recursive higher inductive types only make sense with reference to Pi-types, which are not geometric.)
Traditionally the types in geometric homotopy type theory, hence the geometric homotopy types, are known as ∞-stacks and maybe better as (∞,1)-sheaves, notably as moduli ∞-stacks.
Last revised on April 22, 2019 at 17:08:55. See the history of this page for a list of all contributions to it.