# HoTT/book

added section 8.7 on SIP (the structure identity principle

petera02 committed Dec 5, 2012
1 parent 6d7f405 commit 8ed8a382218ffa19731ab98723cbbeea1772a4e2
Showing with 185 additions and 1 deletion.
1. +120 −0 #macros.tex#
2. +1 −0 .#macros.tex
3. +2 −0 categories.tex
4. +1 −1 main.tex
5. +47 −0 sip.tex
6. +14 −0 sipnote.tex
 @@ -0,0 +1,120 @@ +%%%% MACROS FOR NOTATION %%%% +% Use these for any notation where there are multiple options. + +%%% Definitional equality (used infix) %%% +\newcommand{\jdeq}{\equiv} % An equality judgment +\let\judgeq\jdeq +\newcommand{\defeq}{\coloneqq} % An equality currently being defined + +%%% Identity types %%% +\newcommand{\id}[3][]{\ensuremath{#2 =_{#1} #3}\xspace} +\newcommand{\idtype}[3][]{\ensuremath{\mathsf{Id}_{#1}(#2,#3)}\xspace} + +%%% Reflexivity terms %%% +\newcommand{\refl}[1]{\ensuremath{\mathsf{refl}_{#1}}\xspace} + +%%% Path concatenation (used infix) %%% +\newcommand{\ct}{\mathrel{\raisebox{.5ex}{$\centerdot$}}} + +%%% Path reversal %%% +\newcommand{\opp}[1]{\mathord{!{#1}}} +\let\rev\opp + +%%% Transport %%% +\newcommand{\trans}[2]{\ensuremath{{#1}_{\#}\left({#2}\right)}\xspace} + +%%% Map on paths %%% +\newcommand{\map}[2]{\ensuremath{{#1}_{*}\left({#2}\right)}\xspace} +\newcommand{\mapdep}[2]{\ensuremath{{#1}_{**}\left({#2}\right)}\xspace} + +%%% Identity functions %%% +\newcommand{\idfunc}[1][]{\ensuremath{\mathsf{id}_{#1}}\xspace} + +%%% Equivalence types %%% +\newcommand{\eqv}[2]{\ensuremath{#1 \simeq #2}\xspace} + +%%% Universe types %%% +\newcommand{\type}{\ensuremath{\mathsf{Type}}\xspace} +\newcommand{\set}{\ensuremath{\mathsf{Set}}\xspace} +\newcommand{\prop}{\ensuremath{\mathsf{Prop}}\xspace} + + +%%%% THEOREM ENVIRONMENTS %%%% + +% Hyperref includes the command \autoref{...} which is like \ref{...} +% except that it automatically inserts the type of the thing you're +% referring to, e.g. it produces "Theorem 3.8" instead of just "3.8" +% (and makes the whole thing a hyperlink). This saves a slight amount +% of typing, but more importantly it means that if you decide later on +% that 3.8 should be a Lemma or a Definition instead of a Theorem, you +% don't have to change the name in all the places you referred to it. + +% The following hack improves on this by using the same counter for +% all theorem-type environments, so that after Theorem 1.1 comes +% Corollary 1.2 rather than Corollary 1.1. This makes it much easier +% for the reader to find a particular theorem when flipping through +% the document. +\makeatletter +\def\defthm#1#2{% + %% All types of theorems are numbered inside sections + \newtheorem{#1}{#2}[section]% + %% This command tells hyperref's \autoref what to call things + \expandafter\def\csname #1autorefname\endcsname{#2}% + %% This makes all the theorem counters secretly the same counter + \expandafter\let\csname c@#1\endcsname\c@thm} + +% Now define a bunch of theorem-type environments. +\newtheorem{thm}{Theorem}[section] +\newcommand{\thmautorefname}{Theorem} +%\defthm{prop}{Proposition} % Probably we shouldn't use "Proposition" in this way +\defthm{cor}{Corollary} +\defthm{lem}{Lemma} +% Since definitions and theorems in type theory are synonymous, should +% we actually use the same theoremstyle for them? +\theoremstyle{definition} +\defthm{defn}{Definition} +\theoremstyle{remark} +\defthm{rmk}{Remark} +\defthm{eg}{Example} +\defthm{egs}{Examples} +\defthm{notes}{Notes} +% Number exercises within chapters, with their own counter. +\newtheorem{ex}{Exercise}[chapter] +\def\exautorefname{Exercise} + + +%%%% EQUATION NUMBERING %%%% + +% The following hack uses the single theorem counter to number +% equations as well, so that we don't have both Theorem 1.1 and +% equation (1.1). +\let\c@equation\c@thm +\numberwithin{equation}{section} + + +%%%% ENUMERATE NUMBERING %%%% + +% Number the first level of enumerates as (i), (ii), ... +\renewcommand{\theenumi}{(\roman{enumi})} +\renewcommand{\labelenumi}{\theenumi} + + +%%%% MARGINS %%%% + +% This is a matter of personal preference, but I think the left +% margins on enumerates and itemizes are too wide. +\setitemize[1]{leftmargin=2em} +\setenumerate[1]{leftmargin=*} + +% Likewise that they are too spaced out. +\setitemize[1]{itemsep=-0.2em} +\setenumerate[1]{itemsep=-0.2em} + +%%%% CITATIONS %%%% + +\renewcommand{\cite}[1]{\citep{#1}} + +% Local Variables: +% mode: latex +% TeX-master: "main" +% End:
 @@ -841,7 +841,9 @@ \section*{Exercises} \end{itemize} \end{ex} +\input{sip} % Local Variables: % TeX-master: "main" % End: +
 @@ -37,7 +37,7 @@ \include{computational} \include{categories} - +\include{sip} \include{setmath} \bibliographystyle{abbrvnat}
47 sip.tex
 @@ -0,0 +1,47 @@ +\newpage + +\section{The Structure Identity Principle} +\label{sec:sip} +The {\em Structure Identity Principle (SIP)} is an informal principle +that expresses that isomorphic structures are identical. We aim to +prove a general abstract result which can be applied to a wide family +of notions of structure, where structures may be many-sorted or even +dependently-sorted, they may be infinitary and they may be higher +order. + +The simplest kind of single-sorted structure consists of a type with +no additional structure. The Univalence Axiom expresses SIP for that +notion of structure in a strong form: For types $A,B$, the +canonical function $EAB: (A=B)\ra (A\simeq B)$ such that +$EAA\refl{A}=1_A$, for each type $A$, is an equivalence. + +We start with a precategory $X$. In application to SIP for +single-sorted first order structures $X$ will be the category of sets. +We will define a precategory of $\Omega$-structures, $A = +Str_\Omega(X)$ over $X$, for an abstract signature $\Omega = (P,H)$, +where $Px$ is a set for $x:X$ and $H$ will be specified below. The +type of objects of $A$ is the type $A_0 = \Sigma_{x:X}\; Px$. If +$a=(x,\alpha):A_0$ then let $|a| := x$. $H$ assigns to $a,b:A_0$ and +$f:|a|\ra |b|$ a proposition $Habf$. This function $H$ must satisfy +the following conditions. +\begin{enumerate} +\item $Haa1_a$ for $a:A_0$. +\item $Habf\ra Hbcg\ra Hac(g\circ f)$ for $a,b,c:A_0$ and $f:|a|\ra |b|$, $g:|b|\ra |c|$. +\item $\leq_x$ is a partial order for $x:X_0$ where, for $\alpha,\alpha':Px$, + $\alpha\leq_x\alpha'\; := H(x,\alpha)(x,\alpha')1_x.$ +\end{enumerate} +Note that (i) expresses the reflexivity of each $\leq_x$ and (ii) +implies the transitivity of each $\leq_x$. So that (iii) only adds to +(i) and (ii) the anti-symmetry property of a partial order. If only +(i) and (ii) hold we call $\Omega$ a pre-signature. + +It should now be clear, given a precategory $X$ and a presignature +$\Omega =(P,H)$, how to make $A_0$ into a precategory with type $A_0$ +of objects and, for objects $a,b$, the set $hom_A(a,b) := +\Sigma_{f:|a|\ra |b|}Habf$ of maps $f:a\ra b$. + +Our abstract form of SIP is the following result. +\begin{thm} \label{thm:sip} +If $X$ is a category and $\Omega$ is a signature then the precategory +$Str_\Omega(X)$ is a category. +\end{thm}
 @@ -0,0 +1,14 @@ +\documentclass[12pt]{article} +\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs} +\usepackage{enumitem,mathtools,xspace,xcolor} +\definecolor{darkgreen}{rgb}{0,0.45,0} +\usepackage[pagebackref,colorlinks,citecolor=darkgreen,linkcolor=darkgreen]{hyperref} +\usepackage[all]{xy} +\usepackage{natbib} +\input{macros} +\input{pa-macros} + +\begin{document} +\input{sip.tex} + +\end{document}