nLab
sub-(infinity,1)-category - internal formulation

under construction

Context

Type theory

,

  • ,

    • \vdash ,

(, , , )

  • ,

  • / ()

  • // ()

= + +

/-/
,
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)

  • ,

  • ,

    • , ,

  • ,

Notions of subcategory

    • , , , , , ,

    • , ,

  • ()

    • ()

    • ()

  • (of a )

Contents

Idea

The following gives a characterization of full sub-(∞,1)-categories of an (∞,1)-topos entirely in terms of its internal logic/homotopy type theory.

Background and subtleties

(…)

Statement

(…)

Last revised on December 20, 2011 at 22:44:09. See the history of this page for a list of all contributions to it.