Skip to content

Commit

Permalink
also removed uniqueness for dependent pair types from symbol list
Browse files Browse the repository at this point in the history
  • Loading branch information
EgbertRijke committed Oct 14, 2014
1 parent 1f3d693 commit 76dbf66
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion symbols.tex
Expand Up @@ -255,7 +255,6 @@ \chapter*{Index of symbols}
%%%%%%%%%% U %%%%%%%%%%
\symbolindex{$\nameless$ }{an unnamed object or variable}
\symbolindex{$A \cup B$ }{union of subsets, \pg{union}}
\symbolindex{$\uniq{\sm{x:A}P(x)}$}{uniqueness principle for dependent pair type $\sm{x:A}P(x)$, \pg{thm:eta-sigma}}
\symbolindex{$\uniq{A\times B}$ }{uniqueness principle for the product $A\times B$, \pg{uniquenessproduct}}
\symbolindex{$\uniq{\unit}$ }{uniqueness principle for $\unit$, \pg{uniquenessunit}}
\symbolindex{$\UU$ }{universe type, \pg{sec:universes}}
Expand Down

0 comments on commit 76dbf66

Please sign in to comment.