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

under construction

Context

Type theory

natural deduction metalanguage, practical foundations

judgement
hypothetical judgement, sequent
- antecedents $⊢$ consequent, succedents

type theory (dependent, intensional, observational type theory, homotopy type theory)

calculus of constructions

syntax object language

theory, axiom
proposition/type (propositions as types)
definition/proof/program (proofs as programs)
theorem

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logic	category theory	type theory
true	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	initial object	empty type
proposition	(-1)-truncated object	h-level 1-type/h-prop
proof	generalized element	program
conjunction	product	product type
disjunction	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	internal hom	function type
negation	internal hom into initial object	function type into empty type
universal quantification	dependent product	dependent product type
existential quantification	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
equivalence	path space object	identity type
equivalence class	quotient	quotient type
induction	colimit	inductive type, W-type, M-type
higher induction	higher colimit	higher inductive type
completely presented set	discrete object/0-truncated object	h-level 2-type/preset/h-set
set	internal 0-groupoid	Bishop set/setoid
universe	object classifier	type of types
modality	closure operator monad	modal type theory, monad (in computer science)

homotopy levels

Edit this sidebar

Notions of subcategory

Contents

Idea
Background and subtleties
Statement
References

Idea

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

Background and subtleties

(…)

Statement

(…)

References

Coq-code for lex reflective subcategories in homotopy type theory is at

Mike Shulman, ReflectiveSubcategory.v

Revised on November 21, 2011 16:50:41 by Urs Schreiber (82.113.99.46)