,
,
(, , , )
,
/ ()
// ()
= + +
/ | -/ | |
, | ||
of / of | ||
for | for hom-tensor adjunction | |
introduction rule for | for hom-tensor adjunction | |
( of) | ( of) | |
into | into | |
( of) | ( of) | |
, , | ||
higher | ||
/ | -// | |
/ | ||
, () | , | |
(, ) | / | |
(absence of) | (absence of) | |
,
,
, ,
,
, ,
flavors: , , , , , , , …
models: , , , …
see also
Introductions
Definitions
,
,
,
Paths and cylinders
Homotopy groups
Basic facts
Theorems
-theorem
,
,
,
/
structures in a
/
/
/ homotopy groups
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.
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 17, 2018 at 11:27:51. See the history of this page for a list of all contributions to it.