nLab top

Idea

In a poset $P$, a top of $P$ is a greatest element: an element $\top$ of $P$ such that $a \leq \top$ for every element $a$. Such a top may not exist; if it does, then it is unique.

In a proset, a top may be defined similarly, but it need not be unique. (However, it is still unique up the natural equivalence in the proset.)

A top of $P$ can also be understood as a meet of zero elements in $P$.

A poset that has both top and bottom is called bounded.

As a poset is a special kind of category, a top is simply a terminal object in that category.

The top of the poset of subsets or subobjects of a given set or object $A$ is always $A$ itself.

Related concepts

symbol	in propositional logic	Unicode
$:$	typing relation	U+003A
=	propositional equality relation	U+003D
$\neg$	logical negation operator	U+00AC
$\neg \neg$	double negation	U+00AC&U+00AC
$\nLeftarrow$, $\nleftarrow$	negation of converse implication, or negation of converse conditional	U+21CD, U+219A
$\nLeftrightarrow$, $\nleftrightarrow$	negation of logical equivalence, or negation of biconditional	U+21CE, U+21AE
$\nRightarrow$, $\nrightarrow$	negation of implication, or negation of conditional	U+21CF, U+219B
$\Leftarrow$, $\leftarrow$	converse implication, or converse conditional	U+21D0, U+2190
$\Rightarrow$, $\rightarrow$	implication, or conditional	U+21D2, U+2192
$\Leftrightarrow$, $\leftrightarrow$	logical equivalence, or biconditional	U+21D4, U+2192
$\wedge$	logical conjunctionoperator	U+2227
$\vee$	logical dysjunction operator	U+2228
$\neq$	inequality, or apartness relation	U+2260
$\vdash$	syntactic entailment relation	U+22A2
$\vDash$	semantic entailment relation	U+22A8
$\top$	truth value, or top element	U+22A3
$\bot$	false value, or bottom element	U+22A4
$\veebar$, $\oplus$	logical exclusive dysjunction operator	U+22BB, U+2295
$\bar{\wedge}$	logical non-conjunction operator	U+22BC
$\bar{\vee}$	logical non-dysjunction operator	U+22BD

symbol	in first-order logic	Unicode
$\forall$	universal quantifier	U+2200
$\exists$	existential quantifier	U+2203
$\exists!$	uniqueness quantifier	U+2203&U+0021
$\nexists$	negation of existential quantifier	U+2204

symbol	in set theory	Unicode
×	binary Cartesian product, or binary product	U+00D7
$\varnothing$	empty, or uninhabited set	U+2205
$\in$	membership relation	U+2208
$\notin$	negation of membership relation	U+2209
$\ni$	containment relation	U+220B
$\notni$	negation of containment relation	U+220C
$\prod$	n-ary Cartesian product, or product operator	U+220F
$\coprod$	n-ary disjoint union, or coproduct operator	U+2210
$\cap$	binary intersection operator	U+2229
$\cup$	binary union operator	U+222A
$\subset$	subset of relation	U+2282
$\supset$	superset of relation	U+2283
$\nsubset$	negation of subset relation	U+2284
$\nsupset$	negation of superset relation	U+2285
$\subseteq$	inclusion relation, or subset of, or equal to	U+2286
$\supseteq$	converse of inclusion relation, or superset of, or equal to	U+2287
$\sqcup$	binary disjoint union, or binary coproduct operator	U+2294
$\bigcap$	n-ary intersection operator	U+22C2
$\bigcup$	n-ary union operator	U+22C3

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in linear logic$\phantom{-}$
$\phantom{A}$$\top$	$\phantom{A}$additive truth
$\phantom{A}$$\bot$	$\phantom{A}$additive falsehood
$\phantom{A}$$0$	$\phantom{A}$multiplicative falsehood
$\phantom{A}$$1$	$\phantom{A}$multiplicative truth
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$
$\phantom{A}$$^\bot$$\phantom{A}$	$\phantom{A}$negation$\phantom{A}$

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in dependent type theory$\phantom{-}$	$\phantom{-}$propositions as types$\phantom{-}$
$\phantom{A}$$\to$	$\phantom{A}$function type	$\phantom{A}$implication
$\phantom{A}$$\times$	$\phantom{A}$product type	$\phantom{A}$conjunction
$\phantom{A}$$+$	$\phantom{A}$sum type	$\phantom{A}$disjunction
$\phantom{A}$$0$, $\emptyset$	$\phantom{A}$empty type	$\phantom{A}$false
$\phantom{A}$$1$	$\phantom{A}$unit type	$\phantom{A}$true
$\phantom{A}$$=$, $\mathrm{Id}$	$\phantom{A}$identity type	$\phantom{A}$propositional equality
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types	$\phantom{A}$logical equivalence
$\phantom{A}$$\sum$, $\Sigma$, $\times$	$\phantom{A}$dependent sum type	$\phantom{A}$existential quantifier
$\phantom{A}$$\prod$, $\Pi$, $\to$	$\phantom{A}$dependent product type	$\phantom{A}$universal quantifier
$\phantom{A}$$\mathrm{isContr}$	$\phantom{A}$is contractible type	$\phantom{A}$unique proof
$\phantom{A}$$\mathrm{isContr}(A + B)$	$\phantom{A}$sum type is contractible type	$\phantom{A}$exclusive disjunction
$\phantom{A}$$\mathrm{isContr}\left(\sum_{x:A} B(x)\right)$	$\phantom{A}$dependent sum type is contractible type	$\phantom{A}$uniqueness quantifier
$\phantom{A}$$\mathrm{ua}$	$\phantom{A}$univalence axiom	$\phantom{A}$propositional extensionality