resolve merge conflict

.gitignore

@@ -26,4 +26,222 @@ src/emacs/dependencies
 compile_commands.json
 .ninja_deps
 .ninja_log
-build.ninja
+build.ninja
+
+## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+
+## Intermediate documents:
+*.dvi
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Generated if empty string is given at "Please type another file name for output:"
+.pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+
+## Build tool auxiliary files:
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+
+## Auxiliary and intermediate files from other packages:
+# algorithms
+*.alg
+*.loa
+
+# achemso
+acs-*.bib
+
+# amsthm
+*.thm
+
+# beamer
+*.nav
+*.pre
+*.snm
+*.vrb
+
+# changes
+*.soc
+
+# cprotect
+*.cpt
+
+# elsarticle (documentclass of Elsevier journals)
+*.spl
+
+# endnotes
+*.ent
+
+# fixme
+*.lox
+
+# feynmf/feynmp
+*.mf
+*.mp
+*.t[1-9]
+*.t[1-9][0-9]
+*.tfm
+
+#(r)(e)ledmac/(r)(e)ledpar
+*.end
+*.?end
+*.[1-9]
+*.[1-9][0-9]
+*.[1-9][0-9][0-9]
+*.[1-9]R
+*.[1-9][0-9]R
+*.[1-9][0-9][0-9]R
+*.eledsec[1-9]
+*.eledsec[1-9]R
+*.eledsec[1-9][0-9]
+*.eledsec[1-9][0-9]R
+*.eledsec[1-9][0-9][0-9]
+*.eledsec[1-9][0-9][0-9]R
+
+# glossaries
+*.acn
+*.acr
+*.glg
+*.glo
+*.gls
+*.glsdefs
+
+# gnuplottex
+*-gnuplottex-*
+
+# gregoriotex
+*.gaux
+*.gtex
+
+# hyperref
+*.brf
+
+# knitr
+*-concordance.tex
+# TODO Comment the next line if you want to keep your tikz graphics files
+*.tikz
+*-tikzDictionary
+
+# listings
+*.lol
+
+# makeidx
+*.idx
+*.ilg
+*.ind
+*.ist
+
+# minitoc
+*.maf
+*.mlf
+*.mlt
+*.mtc[0-9]*
+*.slf[0-9]*
+*.slt[0-9]*
+*.stc[0-9]*
+
+# minted
+_minted*
+*.pyg
+
+# morewrites
+*.mw
+
+# nomencl
+*.nlo
+
+# pax
+*.pax
+
+# sagetex
+*.sagetex.sage
+*.sagetex.py
+*.sagetex.scmd
+
+# scrwfile
+*.wrt
+
+# sympy
+*.sout
+*.sympy
+sympy-plots-for-*.tex/
+
+# pdfcomment
+*.upa
+*.upb
+
+# pythontex
+*.pytxcode
+pythontex-files-*/
+
+# thmtools
+*.loe
+
+# TikZ & PGF
+*.dpth
+*.md5
+*.auxlock
+
+# todonotes
+*.tdo
+
+# easy-todo
+*.lod
+
+# xindy
+*.xdy
+
+# xypic precompiled matrices
+*.xyc
+
+# endfloat
+*.ttt
+*.fff
+
+# Latexian
+TSWLatexianTemp*
+
+## Editors:
+# WinEdt
+*.bak
+*.sav
+
+# Texpad
+.texpadtmp
+
+# Kile
+*.backup
+
+# KBibTeX
+*~[0-9]*
+
+# auto folder when using emacs and auctex
+/auto/*
+
+# expex forward references with \gathertags
+*-tags.tex

Notes/smash.tex

@@ -0,0 +1,441 @@
+\documentclass{article}
+
+\input{preamble-articles}
+
+\title{Notes on the smash product}
+\date{\today}
+\usepackage{fullpage}
+\newcommand{\pmap}{\to}
+\newcommand{\lpmap}{\xrightarrow}
+\renewcommand{\smash}{\wedge}
+\renewcommand{\phi}{\varphi}
+\renewcommand{\epsilon}{\varepsilon}
+\newcommand{\tr}{\cdot}
+\renewcommand{\o}{\ensuremath{\circ}}
+\newcommand{\auxl}{\mathsf{auxl}}
+\newcommand{\auxr}{\mathsf{auxr}}
+\newcommand{\gluel}{\mathsf{gluel}}
+\newcommand{\gluer}{\mathsf{gluer}}
+\newcommand{\sy}{^{-1}}
+\newcommand{\const}{\ensuremath{\mathbf{0}}\xspace}
+
+\begin{document}
+
+\maketitle
+
+\section{Pointed Types}
+
+\begin{defn}
+  We work in the $(\infty,1)$-category of pointed types.
+  \begin{itemize}
+  \item The objects are pointed types $A$, types together with a basepoint $a_0:A$.
+\item 1-cells are pointed maps $f:A\to B$ which are maps with a chosen path $f_0:f(a_0)=b_0$. We
+  write $A\pmap B$ for pointed maps and $A\pmap B\pmap C$ means $A\pmap (B\pmap C)$.
+\item 2-cells pointed homotopies. A pointed homotopy $h:f\sim g$ is a homotopy with a chosen 2-path
+  $h(a_0) \tr g_0 = f_0$.
+\item As 3-cells (or higher cells) we take equalities between 2-cells (or higher cells).
+\end{itemize}
+\end{defn}
+
+\begin{rmk}
+\item All types, maps and homotopies in these notes are pointed, unless explicitly mentioned
+  otherwise. Whenever we say that a diagram of $n$-cells commutes we mean it in the sense that there
+  is an $(n+1)$-cell witnessing it.
+\item Pointed homotopies are equivalent to equalities of pointed types: $(f\sim g)\equiv (f=g)$. So
+  we could have chosen to define our 2-cells as equalities between 1-cells. We choose not to, since
+  the aforementioned equivalence requires function extensionality. In a type theory where function
+  extensionality doesn't compute (like Lean) it is better to define the type of pointed homotopies
+  manually so that the underlying homotopy of a 2-cell is definitionally equal to the homotopy we
+  started with. In diagrams, we will denote pointed homotopies by equalities, but we always mean
+  pointed homotopies.
+\item The type $A\to B$ of pointed maps from $A$ to $B$ is itself pointed, with as basepoint the
+  constant map $0\equiv0_{A,B}:A\to B$ which has as underlying function $\lam{a:A}b_0$. We have
+  $0\o g \sim 0$ and $f \o 0 \sim 0$.
+\item A pointed equivalence is a pointed map $f : A \to B$ whose underlying map is an
+  equivalence. In this case, we can find a pointed map $f\sy:B\to A$ with pointed homotopies
+  $f\o f\sy\sim0$ and $f\sy\o f\sim0$.
+\end{rmk}
+
+\begin{lem}
+  Given maps $f:A'\pmap A$ and $g:B\pmap B'$. Then there are maps
+  $(f\pmap C):(A\pmap C)\pmap(A'\pmap C)$ and $(C\pmap g):(C\pmap B)\pmap(C\pmap B')$ given by
+  precomposition with $f$, resp. postcomposition with $g$. The map $\lam{g}C\pmap g$ preserves the basepoint, giving rise to a map $$(C\pmap ({-})):(B\pmap B')\pmap(C\pmap B)\pmap(C\pmap B').$$
+  Also, the following square commutes
+\begin{center}
+\begin{tikzcd}
+(A\pmap B) \arrow[r,"A\pmap g"]\arrow[d,"f\pmap B"] & (A\pmap B')\arrow[d,"f\pmap B'"] \\
+(A'\pmap B) \arrow[r,"A'\pmap g"] & (A'\pmap B')
+\end{tikzcd}
+\end{center}
+
+\end{lem}
+
+
+\section{Smash Product}
+
+\begin{defn}
+  The smash of $A$ and $B$ is the HIT generated by the point constructor $(a,b)$ for $a:A$ and $b:B$
+  and two auxilliary points $\auxl,\auxr:A\smash B$ and path constructors $\gluel_a:(a,b_0)=\auxl$
+  and $\gluer_b:(a_0,b)=\auxr$ (for $a:A$ and $b:B$). $A\smash B$ is pointed with point $(a_0,b_0)$.
+\end{defn}
+\begin{rmk}
+\item This definition of $A\smash B$ is basically the pushout of
+  $\bool\leftarrow A+B\to A \times B$.  A more traditional definition of $A\smash B$ is the pushout
+  $\unit\leftarrow A\vee B\to A \times B$. Here $\vee$ denotes the wedge product, which can be
+  equivalently described as either the pushout $A\leftarrow \unit\to B$ or
+  $\unit\leftarrow \bool\to A + B$. These two definitions of $A\smash B$ are equivalent, because in
+  the following diagram the top-left square and the top rectangle are pushout squares, hence the
+  top-right square is a pushout square by applying the pushout lemma. Another application of the
+  pushout lemma now states that the two definitions of $A\smash B$ are equivalent.
+\begin{center}
+\begin{tikzcd}
+\bool \arrow[r]\arrow[d] & A+B     \arrow[r]\arrow[d] & \bool \arrow[d] \\
+\unit \arrow[r]          & A\vee B \arrow[r]\arrow[d] & \unit \arrow[d] \\
+                     & A\times B        \arrow[r] & A\smash B
+\end{tikzcd}
+\end{center}
+
+\end{rmk}
+\begin{lem}\mbox{}\label{lem:smash-general}
+  \begin{itemize}
+  \item The smash is functorial: if $f:A\pmap A'$ and $g:B\pmap B'$ then
+    $f\smash g:A\smash B\pmap A'\smash B'$. We write $A\smash g$ or $f\smash B$ if one of the
+    functions is the identity function.
+  \item Smash preserves composition, which gives rise to the interchange law:
+    $i:(f' \o f)\smash (g' \o g) \sim f' \smash g' \o f \smash g$
+  \item If $p:f\sim f'$ and $q:g\sim g'$ then $p\smash q:f\smash g\sim f'\smash g'$. This operation
+    preserves reflexivities, symmetries and transitivies.
+  \item There are homotopies $f\smash0\sim0$ and $0\smash g\sim 0$ such that the following diagrams
+    commute for given homotopies $p : f\sim f'$ and $q : g\sim g'$.
+    \begin{center}
+\begin{tikzcd}
+f\smash 0 \arrow[rr, equals,"p\smash1"]\arrow[dr,equals] & &
+f'\smash 0\arrow[dl,equals] \\
+& 0 &
+\end{tikzcd}
+\qquad
+\begin{tikzcd}
+0\smash g\arrow[rr, equals,"1\smash q"]\arrow[dr,equals] & &
+0\smash g'\arrow[dl,equals] \\
+& 0 &
+\end{tikzcd}
+\end{center}
+
+  \end{itemize}
+\end{lem}
+
+\begin{lem}\label{lem:smash-coh}
+  Suppose that we have maps $A_1\lpmap{f_1}A_2\lpmap{f_2}A_3$ and $B_1\lpmap{g_1}B_2\lpmap{g_2}B_3$
+  and suppose that either $f_1$ or $f_2$ is constant. Then there are two homotopies
+  $(f_2 \o f_1)\smash (g_2 \o g_1)\sim 0$, one which uses interchange and one which doesn't. These two
+  homotopies are equal. Specifically, the following two diagrams commute:
+\begin{center}
+\begin{tikzcd}
+(f_2 \o 0)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] &
+(f_2 \smash g_2)\o (0 \smash g_1)\arrow[d,equals] \\
+& (f_2 \smash g_2)\o 0\arrow[d,equals] \\
+0\smash (g_2 \o g_1) \arrow[r,equals] &
+0
+\end{tikzcd}
+\qquad
+\begin{tikzcd}
+(0 \o f_1)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] &
+(0 \smash g_2)\o (f_1 \smash g_1)\arrow[d,equals] \\
+& 0\o (f_1 \smash g_1)\arrow[d,equals] \\
+0\smash (g_2 \o g_1) \arrow[r,equals] &
+0
+\end{tikzcd}
+\end{center}
+
+\end{lem}
+\begin{proof}
+  We will only do the case where $f_1\jdeq 0$, i.e. fill the diagram on the left. The other case is
+  similar (and slightly easier). First apply induction on the paths that $f_2$, $g_1$ and $g_2$
+  respect the basepoint. In this case $f_2\o0$ is definitionally equal to $0$, and the canonical
+  proof that $f_2\o 0\sim0$ is (definitionally) equal to reflexivity. This means that the homotopy
+  $(f_2 \o 0)\smash (g_2 \o g_1)\sim0\smash (g_2 \o g_1)$ is also equal to reflexivity, and also the
+  path that $f_2 \smash g_2$ respects the basepoint is reflexivity, hence the homotopy
+  $(f_2 \smash g_2)\o 0\sim0$ is also reflexivity. This means we need to fill the following square,
+  where $q$ is the proof that $0\smash f\sim 0$.
+\begin{center}
+\begin{tikzcd}
+(f_2 \o 0)\smash (g_2 \o g_1) \arrow[r, equals,"i"]\arrow[d,equals,"1"] &
+(f_2 \smash g_2)\o (0 \smash g_1)\arrow[d,equals,"(f_2\smash g_2)\o q"] \\
+0\smash (g_2 \o g_1) \arrow[r,equals,"q"] &
+0
+\end{tikzcd}
+\end{center}
+
+  For the underlying homotopy, take $x : A_1\smash B_1$ and apply induction on $x$. Suppose
+  $x\equiv(a,b)$ for $a:A_1$ and $b:B_1$. Then we have to fill the square (denote the basepoints of
+  $A_i$ and $B_i$ by $a_i$ and $b_i$ and we suppress the arguments of $\gluer$). Now
+  $\mapfunc{h\smash k}(\gluer_z)=\gluer_{k(z)}$, so by general groupoid laws we see that the path on
+  the bottom is equal to the path on the right, which means we can fill the square.
+  \begin{center}
+    \begin{tikzcd}
+      (f_2(a_2),g_2(g_1(b)))\arrow[r, equals,"1"]
+      \arrow[d,equals,"1"] &
+      % \arrow[d,equals,"\gluer_{g_2(g_1(b))}\tr\gluer_{g_2(g_1(b_1))}\sy"] &
+      (f_2(a_2),g_2(g_1(b)))\arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"] \\
+      (a_3,g_2(g_1(b))) \arrow[r,equals,"\gluer\tr\gluer\sy"] &
+      (a_3,b_3)
+    \end{tikzcd}
+  \end{center}
+  If $x$ is either $\auxl$ or $\auxr$ it is similar but easier. For completeness, we will write down the square we have to fill in the case that $x$ is $\auxr$.
+  \begin{center}
+    \begin{tikzcd}
+      \auxr \arrow[r, equals,"1"]
+      \arrow[d,equals,"1"] &
+      \auxr \arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer_{b_2}\sy)"] \\
+      \auxr \arrow[r,equals,"\gluer_{g_2(b_2)}\sy"] &
+      (a_3,b_3)
+    \end{tikzcd}
+  \end{center}
+  
+  If $x$ varies over $\gluer_b$, we need to fill the cube below. The front and the back are the
+  squares we just filled, the left square is a degenerate square, and the other three squares are
+  the squares in the definition of $q$ and $i$ to show that they respect $\gluer_b$ (and on the
+  right we apply $f_2\smash g_2$ to that square).
+  \begin{center}
+    \begin{tikzcd}
+      & \auxr \arrow[rr, equals,"1"] \arrow[dd,equals,near start,"1"] & &
+      \auxr \arrow[dd,equals,"\mapfunc{f_2\smash g_2}(\gluer_{b_2}\sy)"] \\
+      (f_2(a_2),g_2(g_1(b)))\arrow[rr, equals, near start, crossing over, "1"]
+      \arrow[dd,equals,"1"] \arrow[ur,equals] & &
+      (f_2(a_2),g_2(g_1(b))) \arrow[ur,equals] & \\
+      & \auxr \arrow[rr,equals,near start, "\gluer_{g_2(b_2)}\sy"] & & (a_3,b_3) \\
+      (a_3,g_2(g_1(b))) \arrow[rr,equals,"\gluer\tr\gluer\sy"] \arrow[ur,equals] & &
+      (a_3,b_3) \arrow[from=uu, equals, crossing over, very near start, "\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"]       \arrow[ur,equals] &
+    \end{tikzcd}
+  \end{center}
+  After canceling applications of
+  $\mapfunc{h\smash k}(\gluer_z)=\gluer_{k(z)}$ on various sides of the squares (TODO).
+
+  
+  If $x$ varies over $\gluel_a$ the proof is very similar. Only in the end we need to fill the
+  following cube instead (TODO).
+
+  To show that this homotopy is pointed, (TODO)
+
+\end{proof}
+
+\begin{thm}\label{thm:smash-functor-right}
+Given pointed types $A$, $B$ and $C$, the functorial action of the smash product induces a map
+$$({-})\smash C:(A\pmap B)\pmap(A\smash C\pmap B\smash C)$$
+which is natural in $A$, $B$ and $C$. (note: $(A\smash C\pmap B\smash C)$ is both covariant and contravariant in $C$).
+\end{thm}
+\begin{proof}
+  First note that $\lam{f}f\smash C$ preserves the basepoint so that the map is indeed pointed. We
+  show that this map is natural in each of its arguments individually, which means we need to fill
+  the following squares for $f : A' \to A$ $g:B\to B'$ and $h:C\to C'$.
+\begin{center}
+\begin{tikzcd}
+(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"f\pmap B"] &
+(A\smash C\pmap B\smash C)\arrow[d,"f\smash C\pmap B\smash C"] \\
+(A'\pmap B) \arrow[r,"({-})\smash C"] &
+(A'\smash C\pmap B\smash C)
+\end{tikzcd}
+\begin{tikzcd}
+(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"A\pmap g"] &
+(A\smash C\pmap B\smash C)\arrow[d,"A\smash C\pmap g\smash C"] \\
+(A\pmap B') \arrow[r,"({-})\smash C"] &
+(A\smash C\pmap B'\smash C)
+\end{tikzcd}
+\begin{tikzcd}[column sep=large]
+(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"({-})\smash C'"] &
+(A\smash C\pmap B\smash C)\arrow[d,"A\smash C\pmap B\smash h"] \\
+(A\smash C'\pmap B\smash C') \arrow[r,"A\smash h\pmap B\smash C'"] &
+(A\smash C\pmap B\smash C')
+\end{tikzcd}
+\end{center}
+Let $k:A\pmap B$. Then as homotopy the naturality in $A$ becomes
+$(k\o f)\smash C=k\smash C\o f\smash C$. To prove an equality between pointed maps, we need to give
+a pointed homotopy, which is given by interchange. To show that this homotopy is pointed, we need to
+fill the following square (after reducing out the applications of function extensinality), which follows from \autoref{lem:smash-coh}. 
+\begin{center}
+\begin{tikzcd}
+(0 \o f)\smash C \arrow[r, equals]\arrow[dd,equals] &
+(0 \smash C)\o (f \smash C)\arrow[d,equals] \\
+& 0 \o (f \smash C)\arrow[d,equals] \\
+0\smash C \arrow[r,equals] &
+0
+\end{tikzcd}
+\end{center}
+The naturality in $B$ is almost the same: for the underlying homotopy we need to show
+$(g \o k)\smash C = g\smash C \o k\smash C$. For the pointedness we need to fill the following
+square, which follows from \autoref{lem:smash-coh}.
+\begin{center}
+\begin{tikzcd}
+(g \o 0)\smash C \arrow[r, equals]\arrow[dd,equals] &
+(g \smash C)\o (0 \smash C)\arrow[d,equals] \\
+& (g\smash C) \o 0\arrow[d,equals] \\
+0\smash C \arrow[r,equals] &
+0
+\end{tikzcd}
+\end{center}
+The naturality in $C$ is a bit harder. For the underlying homotopy we need to show
+$B\smash h\o k\smash C=k\smash C'\o A\smash h$. This follows by applying interchange twice:
+$$B\smash h\o k\smash C\sim(\idfunc[B]\o k)\smash(h\o\idfunc[C])\sim(k\o\idfunc[A])\smash(\idfunc[C']\o h)\sim k\smash C'\o A\smash h.$$
+To show that this homotopy is pointed, we need to fill the following square:
+\begin{center}
+  \begin{tikzcd}
+    B\smash h\o 0\smash C \arrow[r, equals]\arrow[d,equals] & 
+    (\idfunc[B]\o 0)\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
+    (0\o\idfunc[A])\smash(\idfunc[C']\o h)\arrow[r, equals]\arrow[d,equals] &
+    0\smash C'\o A\smash h\arrow[d,equals] \\
+    B\smash h\o 0 \arrow[d,equals] & 
+    0\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
+    0\smash(\idfunc[C']\o h) \arrow[d,equals] &
+    0\o A\smash h\arrow[d,equals] \\
+    B\smash h\o 0 \arrow[r, equals] & 
+    0 \arrow[r, equals] &
+    0 \arrow[r, equals] &
+    0
+  \end{tikzcd}
+\end{center}
+The left and the right squares are filled by \autoref{lem:smash-coh}. The squares in the middle
+are filled by (corollaries of) \autoref{lem:smash-general}.
+\end{proof}
+
+\section{Adjunction}
+
+\begin{lem}
+  There is a unit $\eta_{A,B}\equiv\eta:A\pmap B\pmap A\smash B$ and counit
+  $\epsilon_{B,C}\equiv\epsilon : (B\pmap C)\smash B \pmap C$ which are natural in both arguments
+  and satisfy the unit-counit laws:
+  $$(A\to\epsilon_{A,B})\o \eta_{A\to B,A}\sim \idfunc[A\to B]\qquad
+  \epsilon_{B,B\smash C}\o \eta_{A,B}\smash B\sim\idfunc[A\smash B].$$
+  
+
+\end{lem}
+\begin{proof}
+  We define $\eta ab=(a,b)$. Then $\eta a$ respects the basepoint because
+  $(a,b_0)=(a_0,b_0)$. Also, $\eta$ itself respects the basepoint. To show this, we need to show
+  that $\eta a_0\sim0$. The underlying maps are homotopic, since $(a_0,b)=(a_0,b_0)$. To show that
+  this homotopy is pointed, we need to show that the two given proofs of $(a_0,b_0)=(a_0,b_0)$ are
+  equal, but they are both equal to reflexivity:
+  $$\gluel_{a_0}\tr\gluel_{a_0}\sy=1=\gluer_{b_0}\tr\gluer_{b_0}\sy.$$
+  This defines the unit. To define the counit, given $x:(B\pmap C)\smash B$. We construct
+  $\epsilon x:C$ by induction on $x$. If $x\jdeq(f,b)$ we set $\epsilon(f,b)\defeq f(b)$. If $x$
+  is either $\auxl$ or $\auxr$ then we set $\epsilon x\defeq c_0:C$. If $x$ varies over $\gluel_f$
+  then we need to show that $f(b_0)=c_0$, which is true by $f_0$. If $x$ varies over $\gluer_b$ we
+  need to show that $0(b)=c_0$ which is true by reflexivity. $\epsilon$ is trivially a pointed map,
+  which defines the counit.
+
+  Now we need to show that the unit and counit are natural. (TODO).
+
+  Finally we need to show that unit-counit laws. For the underlying homotopy of the first one, let
+  $f:A\to B$. We need to show that $p:\epsilon\o\eta f\sim f$. For the underlying homotopy of $p$,
+  let $a:A$, and we need to show that $\epsilon(f,a)=f(a)$, which is true by reflexivity. To show
+  that $p$ is a pointed homotopy, we need to show that
+  $p(a_0)\tr f_0=\mapfunc{\epsilon}(\eta f)_0\tr \epsilon_0$, which reduces to
+  $f_0=\mapfunc{\epsilon}(\gluel_f\tr\gluel_0\sy)$, but we can reduce the right hand side: (note:
+  $0_0$ denotes the proof that $0(a_0)=b_0$, which is reflexivity)
+  $$\mapfunc{\epsilon}(\gluel_f\tr\gluel_0\sy)=\mapfunc{\epsilon}(\gluel_f)\tr(\mapfunc{\epsilon}(\gluel_0))\sy=f_0\tr 0_0\sy=f_0.$$
+  Now we need to show that $p$ itself respects the basepoint of $A\to B$, i.e. that the composite
+  $\epsilon\o\eta0\sim\epsilon\o0\sim0$ is equal to $p$ for $f\equiv 0_{A,B}$. The underlying
+  homotopies are the same for $a : A$; on the one side we have
+  $\mapfunc{\epsilon}(\gluer_{a}\tr\gluer_{a_0}\sy)$ and on the other side we have reflexivity
+  (note: this typechecks, since $0_{A,B}a\equiv0_{A,B}a_0$). These paths are equal, since
+  $$\mapfunc{\epsilon}(\gluer_{a}\tr\gluer_{a_0}\sy)=\mapfunc{\epsilon}(\gluer_{a})\tr(\mapfunc\epsilon(\gluer_{a_0}))\sy=1\cdot1\sy\equiv1.$$
+  Both pointed homotopies are pointed in the same way, which requires some path-algebra, and we skip
+  the proof here.
+
+  For the underlying homotopy of the second one, we need to show for $x:A\smash B$ that
+  $\epsilon(\eta\smash B(x))=x$, which we prove by induction to $x$. (TODO).
+
+\end{proof}
+
+\begin{defn}
+The function $e\jdeq e_{A,B,C}:(A\pmap B\pmap C)\pmap(A\smash B\pmap C)$ is defined as the composite
+$$(A\pmap B\pmap C)\lpmap{({-})\smash B}(A\smash B\pmap (B\pmap C)\smash B)\lpmap{A\smash B \pmap\epsilon}(A\smash B\pmap C)).$$
+\end{defn}
+
+\begin{lem}
+  $e$ is invertible, hence gives a pointed equivalence $$(A\pmap B\pmap C)\simeq(A\smash B\pmap C).$$
+\end{lem}
+\begin{proof}
+  Define
+  $$\inv{e}_{A,B,C}:(A\smash B\pmap C)\lpmap{B\pmap({-})}((B\pmap A\smash B)\pmap (B\pmap
+  C))\lpmap{\eta\pmap(B\pmap C)}(A\pmap B\pmap C).$$ It is easy to show that $e$ and $\inv{e}$ are
+  inverses as unpointed maps from the unit-counit laws and naturality of $\eta$ and $\epsilon$.
+
+%   For $f : A\pmap B\pmap C$ we have
+%   \begin{align*}
+%     \inv{e}(e(f))&\equiv(\eta\pmap(B\pmap C))\o (B\pmap((A\smash B\pmap\epsilon)\of\smash B))\\
+%                  &= (\eta\pmap(B\pmap C))\o (B\pmap(A\smash B\pmap\epsilon))\o(B\pmapf\smash B)\\
+% %                 &= (\eta\pmap(B\pmap C))\o (B\pmap(A\smash B\pmap\epsilon))\o(B\pmapf\smash B)\\
+%   \end{align*}
+\end{proof}
+\begin{lem}\label{e-natural}
+$e$ is natural in $A$, $B$ and $C$.
+\end{lem}
+\begin{rmk}
+\item Instead of showing that $e$ is natural, we could instead show that $e^{-1}$ is natural. In
+  that case we need to show that the map $A\to({-}):(B\to C)\to(A\to B)\to(A\to C)$ is natural in
+  $A$, $B$ and $C$. This might actually be easier, since we don't need to work with any higher
+  inductive type to prove that.
+\end{rmk}
+\begin{proof}
+\textbf{$e$ is natural in $A$}. Suppose that $f:A'\pmap A$. Then the following diagram commutes. The left square commutes by naturality of $({-})\smash B$ in the first argument and the right square commutes because composition on the left commutes with composition on the right.
+\begin{center}
+\begin{tikzcd}
+(A\pmap B\pmap C) \arrow[r,"({-})\smash B"]\arrow[d,"f\pmap B\pmap C"] &
+(A\smash B\pmap (B\pmap C)\smash B) \arrow[r,"A\smash B\pmap\epsilon"]\arrow[d,"f\smash B\pmap\cdots"]  &
+(A\smash B\pmap C)\arrow[d,"f\smash B\pmap C"] \\
+(A'\pmap B\pmap C) \arrow[r,"({-})\smash B"] &
+(A'\smash B\pmap (B\pmap C)\smash B) \arrow[r,"A\smash B\pmap\epsilon"] &
+(A'\smash B\pmap C)
+\end{tikzcd}
+\end{center}
+
+\textbf{$e$ is natural in $C$}. Suppose that $f:C\pmap C'$. Then in the following diagram the left square commutes by naturality of $({-})\smash B$ in the second argument (applied to $B\pmap f$) and the right square commutes by applying the functor $A\smash B \pmap({-})$ to the naturality of $\epsilon$ in the second argument.
+\begin{center}
+\begin{tikzcd}
+(A\pmap B\pmap C) \arrow[r]\arrow[d] &
+(A\smash B\pmap (B\pmap C)\smash B) \arrow[r]\arrow[d] &
+(A\smash B\pmap C)\arrow[d] \\
+(A\pmap B\pmap C') \arrow[r] &
+(A\smash B\pmap (B\pmap C')\smash B) \arrow[r] &
+(A\smash B\pmap C')
+\end{tikzcd}
+\end{center}
+
+\textbf{$e$ is natural in $B$}. Suppose that $f:B'\pmap B$. The diagram looks weird since $({-})\smash B$ is both contravariant and covariant in $B$. Then we get the following diagram. The front square commutes by naturality of $({-})\smash B$ in the second argument (applied to $f\pmap C$). The top square commutes by naturality of $({-})\smash B$ in the third argument, the back square commutes because composition on the left commutes with composition on the right, and finally the right square commutes by applying the functor $A\smash B' \pmap({-})$ to the naturality of $\epsilon$ in the first argument.
+\begin{center}
+\begin{tikzcd}[row sep=scriptsize, column sep=-4em]
+& (A\smash B\pmap (B\pmap C)\smash B) \arrow[rr] \arrow[dd] & & (A\smash B'\pmap (B\pmap C)\smash B)\arrow[dd] \\
+(A\pmap B\pmap C) \arrow[ur] \arrow[rr, crossing over] \arrow[dd] & & (A\smash B'\pmap (B\pmap C)\smash B') \arrow[ur] \\
+& (A\smash B\pmap C)\arrow[rr] &  & (A\smash B'\pmap C) \\
+(A\pmap B'\pmap C) \arrow[rr] & & (A\smash B'\pmap (B'\pmap C)\smash B') \arrow[ur] \arrow[from=uu, crossing over]\\
+\end{tikzcd}
+\end{center}
+
+\end{proof}
+
+\begin{thm}
+  The smash product is associative: there is an equivalence $f : A \smash (B \smash C) \simeq (A \smash B) \smash C$ which is natural in $A$, $B$ and $C$.
+\end{thm}
+\begin{proof}
+  Let $\phi_X$ be the composite of the following equivalences:
+  \begin{align*}
+    A \smash (B \smash C)\to X&\simeq A \to B\smash C\to X\\
+    &\simeq A \to B\to C\to X\\
+    &\simeq A \smash B\to C\to X\\
+    &\simeq (A \smash B)\smash C\to X.                              
+  \end{align*}
+  $\phi_X$ is natural in $A,B,C,X$ by repeatedly applying \autoref{e-natural}. Let
+  $f\defeq\phi_{A \smash (B \smash C)}(\idfunc)$ and
+  $f\sy\defeq\phi\sy_{(A \smash B) \smash C}(\idfunc)$. Now these maps are inverses by naturality of
+  $\phi$ in $X$:
+  $$f\sy\o f\equiv f\sy\o \phi(\idfunc)\sim \phi(f\sy\o\idfunc)\sim \phi(\phi\sy(\idfunc))\sim\idfunc.$$
+  The other composition is the identity by a similar argument. Lastly, $f$ is natural in $A$, $B$
+  and $C$, since $\phi_X$ is.
+\end{proof}
+
+\section{Notes on the formalization}
+
+The order of arguments are different in the formalization here and there.
+Also, some smashes are commuted. This is because some unfortunate choices have been made in the formalization. Reversing these choices is possible, but probably more work than it's worth (the final result is exactly the same).
+
+\end{document}

algebra/graded.hlean

@@ -1,7 +1,175 @@
-/-
-Copyright (c) 2016 Egbert Rijke. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Egbert Rijke
+/- Graded (left-) R-modules for a ring R. -/
 
-Graded modules and rings.
+-- Author: Floris van Doorn
+
+import .left_module
+
+open algebra eq left_module pointed function equiv is_equiv is_trunc prod
+
+namespace left_module
+
+definition graded (str : Type) (I : Type) : Type := I → str
+definition graded_module (R : Ring) : Type → Type := graded (LeftModule R)
+
+variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}
+
+/-
+  morphisms between graded modules.
+  The definition is unconventional in two ways:
+  (1) The degree is determined by an endofunction instead of a element of I (and in this case we
+    don't need to assume that I is a group). The "standard" degree i corresponds to the endofunction
+    which is addition with i on the right. However, this is more flexible. For example, the
+    composition of two graded module homomorphisms φ₂ and φ₁ with degrees i₂ and i₁ has type
+    M₁ i → M₂ ((i + i₁) + i₂).
+    However, a homomorphism with degree i₁ + i₂ must have type
+    M₁ i → M₂ (i + (i₁ + i₂)),
+    which means that we need to insert a transport. With endofunctions this is not a problem:
+    λi, (i + i₁) + i₂
+    is a perfectly fine degree of a map
+  (2) Since we cannot eliminate all possible transports, we don't define a homomorphism as function
+    M₁ i →lm M₂ (i + deg f)  or  M₁ i →lm M₂ (deg f i)
+    but as a function taking a path as argument. Specifically, for every path
+    deg f i = j
+    we get a function M₁ i → M₂ j.
 -/
+structure graded_hom (M₁ M₂ : graded_module R I) : Type :=
+mk' ::  (d : I → I)
+        (fn' : Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j)
+
+notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂
+
+abbreviation deg [unfold 5] := @graded_hom.d
+notation `↘` := graded_hom.fn' -- there is probably a better character for this?
+
+definition graded_hom_fn [unfold 5] [coercion] (f : M₁ →gm M₂) (i : I) : M₁ i →lm M₂ (deg f i) :=
+↘f idp
+
+definition graded_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I → I)
+  (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
+graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
+
+variables {f' : M₂ →gm M₃} {f : M₁ →gm M₂}
+
+definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
+graded_hom.mk (deg f' ∘ deg f) (λi, f' (deg f i) ∘lm f i)
+
+variable (M)
+definition graded_hom_id [constructor] [refl] : M →gm M :=
+graded_hom.mk id (λi, lmid)
+variable {M}
+
+abbreviation gmid [constructor] := graded_hom_id M
+infixr ` ∘gm `:75 := graded_hom_compose
+
+structure graded_iso (M₁ M₂ : graded_module R I) : Type :=
+  (to_hom : M₁ →gm M₂)
+  (is_equiv_deg : is_equiv (deg to_hom))
+  (is_equiv_to_hom : Π⦃i j⦄ (p : deg to_hom i = j), is_equiv (↘to_hom p))
+
+infix ` ≃gm `:25 := graded_iso
+attribute graded_iso.to_hom [coercion]
+attribute graded_iso.is_equiv_deg [instance] [priority 1010]
+attribute graded_iso._trans_of_to_hom [unfold 5]
+
+definition is_equiv_graded_iso [instance] [priority 1010] (φ : M₁ ≃gm M₂) (i : I) :
+  is_equiv (φ i) :=
+graded_iso.is_equiv_to_hom φ idp
+
+definition isomorphism_of_graded_iso' [constructor] (φ : M₁ ≃gm M₂) {i j : I} (p : deg φ i = j) :
+  M₁ i ≃lm M₂ j :=
+isomorphism.mk (↘φ p) !graded_iso.is_equiv_to_hom
+
+definition isomorphism_of_graded_iso [constructor] (φ : M₁ ≃gm M₂) (i : I) :
+  M₁ i ≃lm M₂ (deg φ i) :=
+isomorphism.mk (φ i) _
+
+definition graded_iso_of_isomorphism [constructor] (d : I ≃ I) (φ : Πi, M₁ i ≃lm M₂ (d i)) :
+  M₁ ≃gm M₂ :=
+begin
+  apply graded_iso.mk (graded_hom.mk d φ), apply to_is_equiv, intro i j p, induction p,
+  exact to_is_equiv (equiv_of_isomorphism (φ i)),
+end
+
+definition graded_iso_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
+  : M₁ ≃gm M₂ :=
+graded_iso_of_isomorphism erfl (λi, isomorphism_of_eq (p i))
+
+-- definition graded_iso.MK [constructor] (d : I ≃ I) (fn : Πi, M₁ i →lm M₂ (d i))
+--   : M₁ ≃gm M₂ :=
+-- graded_iso.mk _ _ _ --d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
+
+definition isodeg [unfold 5] (φ : M₁ ≃gm M₂) : I ≃ I :=
+equiv.mk (deg φ) _
+
+definition graded_iso_to_lminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
+graded_hom.mk (deg φ)⁻¹
+  abstract begin
+    intro i, apply to_lminv,
+    apply isomorphism_of_graded_iso' φ,
+    apply to_right_inv (isodeg φ) i
+  end end
+
+definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
+graded_hom.mk (deg φ)⁻¹
+  abstract begin
+    intro i, apply isomorphism.to_hom, symmetry,
+    apply isomorphism_of_graded_iso' φ,
+    apply to_right_inv (isodeg φ) i
+  end end
+
+variable (M)
+definition graded_iso.refl [refl] [constructor] : M ≃gm M :=
+graded_iso_of_isomorphism equiv.rfl (λi, isomorphism.rfl)
+variable {M}
+
+definition graded_iso.rfl [refl] [constructor] : M ≃gm M := graded_iso.refl M
+
+definition graded_iso.symm [symm] [constructor] (φ : M₁ ≃gm M₂) : M₂ ≃gm M₁ :=
+graded_iso.mk (to_gminv φ) !is_equiv_inv
+  (λi j p, @is_equiv_compose _ _ _ _ _ !isomorphism.is_equiv_to_hom !is_equiv_cast)
+
+definition graded_iso.trans [trans] [constructor] (φ : M₁ ≃gm M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
+graded_iso_of_isomorphism (isodeg φ ⬝e isodeg ψ)
+  (λi, isomorphism_of_graded_iso φ i ⬝lm isomorphism_of_graded_iso ψ (deg φ i))
+
+definition graded_iso.eq_trans [trans] [constructor]
+   {M₁ M₂ : graded_module R I} {M₃ : graded_module R I} (φ : M₁ ~ M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
+proof graded_iso.trans (graded_iso_of_eq φ) ψ qed
+
+definition graded_iso.trans_eq [trans] [constructor]
+  {M₁ : graded_module R I} {M₂ M₃ : graded_module R I} (φ : M₁ ≃gm M₂) (ψ : M₂ ~ M₃) : M₁ ≃gm M₃ :=
+graded_iso.trans φ (graded_iso_of_eq ψ)
+
+postfix `⁻¹ᵍᵐ`:(max + 1) := graded_iso.symm
+infixl ` ⬝gm `:75 := graded_iso.trans
+infixl ` ⬝gmp `:75 := graded_iso.trans_eq
+infixl ` ⬝pgm `:75 := graded_iso.eq_trans
+
+definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
+  : M₁ →gm M₂ :=
+graded_iso_of_eq p
+
+/- exact couples -/
+
+definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
+Π{i j k} (p : deg f i = j) (q : deg f' j = k), is_exact_mod (↘f p) (↘f' q)
+
+structure exact_couple (M₁ M₂ : graded_module R I) : Type :=
+  (i : M₁ →gm M₁) (j : M₁ →gm M₂) (k : M₂ →gm M₁)
+  (exact_ij : is_exact_gmod i j)
+  (exact_jk : is_exact_gmod j k)
+  (exact_ki : is_exact_gmod k i)
+
+  variables {i : M₁ →gm M₁} {j : M₁ →gm M₂} {k : M₂ →gm M₁}
+            (exact_ij : is_exact_gmod i j)
+            (exact_jk : is_exact_gmod j k)
+            (exact_ki : is_exact_gmod k i)
+
+  namespace derived_couple
+
+  definition d : M₂ →gm M₂ := j ∘gm k
+
+  end derived_couple
+
+
+end left_module

algebra/left_module.hlean

@@ -0,0 +1,330 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaniel Thomas, Jeremy Avigad, Floris van Doorn
+
+Modules prod vector spaces over a ring.
+
+(We use "left_module," which is more precise, because "module" is a keyword.)
+-/
+import algebra.field ..move_to_lib
+open is_trunc pointed function sigma eq algebra prod is_equiv equiv
+
+structure has_scalar [class] (F V : Type) :=
+(smul : F → V → V)
+
+infixl ` • `:73 := has_scalar.smul
+
+/- modules over a ring -/
+
+namespace left_module
+
+structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming
+  mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
+  mul_left_inv→add_left_inv mul_comm→add_comm :=
+(smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
+(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add _ r s) x = (add (smul r x) (smul s x)))
+(mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x))
+(one_smul : Π x, smul one x = x)
+
+/- we make it a class now (and not as part of the structure) to avoid
+  left_module.to_ab_group to be an instance -/
+attribute left_module [class]
+
+definition add_ab_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
+  [H : left_module R M] : add_ab_group M :=
+@left_module.to_ab_group R M K H
+
+definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
+  [H : left_module R M] : has_scalar R M :=
+@left_module.to_has_scalar R M K H
+
+section left_module
+  variables {R M : Type}
+  variable  [ringR : ring R]
+  variable  [moduleRM : left_module R M]
+  include   ringR moduleRM
+
+  -- Note: the anonymous include does not work in the propositions below.
+
+  proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
+  !left_module.smul_left_distrib
+
+  proposition smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u :=
+  !left_module.smul_right_distrib
+
+  proposition mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
+  !left_module.mul_smul
+
+  proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul
+
+  proposition zero_smul (u : M) : (0 : R) • u = 0 :=
+  have (0 : R) • u + 0 • u = 0 • u + 0, by rewrite [-smul_right_distrib, *add_zero],
+  !add.left_cancel this
+
+  proposition smul_zero (a : R) : a • (0 : M) = 0 :=
+  have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
+  !add.left_cancel this
+
+  proposition neg_smul (a : R) (u : M) : (-a) • u = - (a • u) :=
+  eq_neg_of_add_eq_zero (by rewrite [-smul_right_distrib, add.left_inv, zero_smul])
+
+  proposition neg_one_smul (u : M) : -(1 : R) • u = -u :=
+  by rewrite [neg_smul, one_smul]
+
+  proposition smul_neg (a : R) (u : M) : a • (-u) = -(a • u) :=
+  by rewrite [-neg_one_smul, -mul_smul, mul_neg_one_eq_neg, neg_smul]
+
+  proposition smul_sub_left_distrib (a : R) (u v : M) : a • (u - v) = a • u - a • v :=
+  by rewrite [sub_eq_add_neg, smul_left_distrib, smul_neg]
+
+  proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v :=
+  by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul]
+end left_module
+
+/- vector spaces -/
+
+structure vector_space [class] (F V : Type) [fieldF : field F]
+  extends left_module F V
+
+/- homomorphisms -/
+
+definition is_smul_hom [class] (R : Type) {M₁ M₂ : Type} [has_scalar R M₁] [has_scalar R M₂]
+  (f : M₁ → M₂) : Type :=
+∀ r : R, ∀ a : M₁, f (r • a) = r • f a
+
+definition is_prop_is_smul_hom [instance] (R : Type) {M₁ M₂ : Type} [is_set M₂]
+  [has_scalar R M₁] [has_scalar R M₂] (f : M₁ → M₂) : is_prop (is_smul_hom R f) :=
+begin unfold is_smul_hom, apply _ end
+
+definition respect_smul (R : Type) {M₁ M₂ : Type} [has_scalar R M₁] [has_scalar R M₂]
+    (f : M₁ → M₂) [H : is_smul_hom R f] :
+  ∀ r : R, ∀ a : M₁, f (r • a) = r • f a :=
+H
+
+definition is_module_hom [class] (R : Type) {M₁ M₂ : Type}
+  [has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
+  (f : M₁ → M₂) :=
+is_add_hom f × is_smul_hom R f
+
+definition is_add_hom_of_is_module_hom [instance] (R : Type) {M₁ M₂ : Type}
+  [has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
+  (f : M₁ → M₂) [H : is_module_hom R f] : is_add_hom f :=
+prod.pr1 H
+
+definition is_smul_hom_of_is_module_hom [instance] {R : Type} {M₁ M₂ : Type}
+  [has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
+  (f : M₁ → M₂) [H : is_module_hom R f] : is_smul_hom R f :=
+prod.pr2 H
+
+-- Why do we have to give the instance explicitly?
+definition is_prop_is_module_hom [instance] (R : Type) {M₁ M₂ : Type}
+  [has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
+  (f : M₁ → M₂) : is_prop (is_module_hom R f) :=
+have h₁ : is_prop (is_add_hom f), from is_prop_is_add_hom f,
+begin unfold is_module_hom, apply _ end
+
+section module_hom
+  variables {R : Type} {M₁ M₂ M₃ : Type}
+  variables [has_scalar R M₁] [has_scalar R M₂] [has_scalar R M₃]
+  variables [add_group M₁] [add_group M₂] [add_group M₃]
+  variables (g : M₂ → M₃) (f : M₁ → M₂) [is_module_hom R g] [is_module_hom R f]
+
+  proposition is_module_hom_id : is_module_hom R (@id M₁) :=
+  pair (λ a₁ a₂, rfl) (λ r a, rfl)
+
+  proposition is_module_hom_comp : is_module_hom R (g ∘ f) :=
+  pair
+    (take a₁ a₂, begin esimp, rewrite [respect_add f, respect_add g] end)
+    (take r a, by esimp; rewrite [respect_smul R f, respect_smul R g])
+
+  proposition respect_smul_add_smul (a b : R) (u v : M₁) : f (a • u + b • v) = a • f u + b • f v :=
+  by rewrite [respect_add f, +respect_smul R f]
+end module_hom
+
+structure LeftModule (R : Ring) :=
+(carrier : Type) (struct : left_module R carrier)
+
+local attribute LeftModule.carrier [coercion]
+attribute LeftModule.struct [instance]
+
+definition pointed_LeftModule_carrier [instance] {R : Ring} (M : LeftModule R) :
+  pointed (LeftModule.carrier M) :=
+pointed.mk zero
+
+definition pSet_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : Set* :=
+pSet.mk' (LeftModule.carrier M)
+
+section
+  variable {R : Ring}
+
+  structure homomorphism (M₁ M₂ : LeftModule R) : Type :=
+    (fn : LeftModule.carrier M₁ → LeftModule.carrier M₂)
+    (p : is_module_hom R fn)
+
+  infix ` →lm `:55 := homomorphism
+
+  definition homomorphism_fn [unfold 4] [coercion] := @homomorphism.fn
+
+  definition is_module_hom_of_homomorphism [unfold 4] [instance] [priority 900]
+      {M₁ M₂ : LeftModule R} (φ : M₁ →lm M₂) : is_module_hom R φ :=
+  homomorphism.p φ
+
+  section
+    variables {M₁ M₂ : LeftModule R} (φ : M₁ →lm M₂)
+
+    definition to_respect_add (x y : M₁) : φ (x + y) = φ x + φ y :=
+    respect_add φ x y
+
+    definition to_respect_smul (a : R) (x : M₁) : φ (a • x) = a • (φ x) :=
+    respect_smul R φ a x
+
+    definition is_embedding_of_homomorphism /- φ -/ (H : Π{x}, φ x = 0 → x = 0) : is_embedding φ :=
+    is_embedding_of_is_add_hom φ @H
+
+    variables (M₁ M₂)
+    definition is_set_homomorphism [instance] : is_set (M₁ →lm M₂) :=
+    begin
+      have H : M₁ →lm M₂ ≃ Σ(f : LeftModule.carrier M₁ → LeftModule.carrier M₂),
+        is_module_hom (Ring.carrier R) f,
+      begin
+        fapply equiv.MK,
+        { intro φ, induction φ, constructor, exact p},
+        { intro v, induction v with f H, constructor, exact H},
+        { intro v, induction v, reflexivity},
+        { intro φ, induction φ, reflexivity}
+      end,
+    have ∀ f : LeftModule.carrier M₁ → LeftModule.carrier M₂,
+      is_set (is_module_hom (Ring.carrier R) f), from _,
+    apply is_trunc_equiv_closed_rev, exact H
+  end
+
+  variables {M₁ M₂}
+  definition pmap_of_homomorphism [constructor] /- φ -/ :
+    pSet_of_LeftModule M₁ →* pSet_of_LeftModule M₂ :=
+  have H : φ 0 = 0, from respect_zero φ,
+  pmap.mk φ begin esimp, exact H end
+
+  definition homomorphism_change_fun [constructor]
+    (φ : M₁ →lm M₂) (f : M₁ → M₂) (p : φ ~ f) : M₁ →lm M₂ :=
+  homomorphism.mk f
+    (prod.mk
+      (λx₁ x₂, (p (x₁ + x₂))⁻¹ ⬝ to_respect_add φ x₁ x₂ ⬝ ap011 _ (p x₁) (p x₂))
+      (λ a x, (p (a • x))⁻¹ ⬝ to_respect_smul φ a x ⬝ ap01 _ (p x)))
+
+  definition homomorphism_eq (φ₁ φ₂ : M₁ →lm M₂) (p : φ₁ ~ φ₂) : φ₁ = φ₂ :=
+  begin
+    induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p,
+    exact ap (homomorphism.mk φ₂) !is_prop.elim
+  end
+end
+
+  section
+  variables {M M₁ M₂ M₃ : LeftModule R}
+
+  definition LeftModule.struct2 [instance] (M : LeftModule R) : left_module R M :=
+  LeftModule.struct M
+
+  definition homomorphism.mk' [constructor] (φ : M₁ → M₂)
+    (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
+    (q : Π(r : R) x, φ (r • x) = r • φ x) : M₁ →lm M₂ :=
+  homomorphism.mk φ (p, q)
+
+  definition to_respect_zero (φ : M₁ →lm M₂) : φ 0 = 0 :=
+  respect_zero φ
+
+  definition homomorphism_compose [constructor] (f' : M₂ →lm M₃) (f : M₁ →lm M₂) : M₁ →lm M₃ :=
+  homomorphism.mk (f' ∘ f) !is_module_hom_comp
+
+  variable (M)
+  definition homomorphism_id [constructor] [refl] : M →lm M :=
+  homomorphism.mk (@id M) !is_module_hom_id
+  variable {M}
+
+  abbreviation lmid [constructor] := homomorphism_id M
+  infixr ` ∘lm `:75 := homomorphism_compose
+
+  structure isomorphism (M₁ M₂ : LeftModule R) :=
+    (to_hom : M₁ →lm M₂)
+    (is_equiv_to_hom : is_equiv to_hom)
+
+  infix ` ≃lm `:25 := isomorphism
+  attribute isomorphism.to_hom [coercion]
+  attribute isomorphism.is_equiv_to_hom [instance]
+  attribute isomorphism._trans_of_to_hom [unfold 4]
+
+  definition equiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃ M₂ :=
+  equiv.mk φ !isomorphism.is_equiv_to_hom
+
+  definition pequiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃* M₂ :=
+  pequiv_of_equiv (equiv_of_isomorphism φ) (to_respect_zero φ)
+
+  definition isomorphism_of_equiv [constructor] (φ : M₁ ≃ M₂)
+    (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
+    (q : Πr x, φ (r • x) = r • φ x) : M₁ ≃lm M₂ :=
+  isomorphism.mk (homomorphism.mk φ (p, q)) !to_is_equiv
+
+  definition isomorphism_of_eq [constructor] {M₁ M₂ : LeftModule R} (p : M₁ = M₂ :> LeftModule R)
+    : M₁ ≃lm M₂ :=
+  isomorphism_of_equiv (equiv_of_eq (ap LeftModule.carrier p))
+    begin intros, induction p, reflexivity end
+    begin intros, induction p, reflexivity end
+
+  -- definition pequiv_of_isomorphism_of_eq {M₁ M₂ : LeftModule R} (p : M₁ = M₂ :> LeftModule R) :
+  --   pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_LeftModule p) :=
+  -- begin
+  --   induction p,
+  --   apply pequiv_eq,
+  --   fapply pmap_eq,
+  --   { intro g, reflexivity},
+  --   { apply is_prop.elim}
+  -- end
+
+  definition to_lminv [constructor] (φ : M₁ ≃lm M₂) : M₂ →lm M₁ :=
+  homomorphism.mk φ⁻¹
+    abstract begin
+    split,
+      intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
+      rewrite [respect_add φ, +right_inv φ],
+      intro r x, apply eq_of_fn_eq_fn' φ,
+      rewrite [to_respect_smul φ, +right_inv φ],
+    end end
+
+  variable (M)
+  definition isomorphism.refl [refl] [constructor] : M ≃lm M :=
+  isomorphism.mk lmid !is_equiv_id
+  variable {M}
+
+  definition isomorphism.rfl [refl] [constructor] : M ≃lm M := isomorphism.refl M
+
+  definition isomorphism.symm [symm] [constructor] (φ : M₁ ≃lm M₂) : M₂ ≃lm M₁ :=
+  isomorphism.mk (to_lminv φ) !is_equiv_inv
+
+  definition isomorphism.trans [trans] [constructor] (φ : M₁ ≃lm M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ :=
+  isomorphism.mk (ψ ∘lm φ) !is_equiv_compose
+
+  definition isomorphism.eq_trans [trans] [constructor]
+     {M₁ M₂ : LeftModule R} {M₃ : LeftModule R} (φ : M₁ = M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ :=
+  proof isomorphism.trans (isomorphism_of_eq φ) ψ qed
+
+  definition isomorphism.trans_eq [trans] [constructor]
+    {M₁ : LeftModule R} {M₂ M₃ : LeftModule R} (φ : M₁ ≃lm M₂) (ψ : M₂ = M₃) : M₁ ≃lm M₃ :=
+  isomorphism.trans φ (isomorphism_of_eq ψ)
+
+  postfix `⁻¹ˡᵐ`:(max + 1) := isomorphism.symm
+  infixl ` ⬝lm `:75 := isomorphism.trans
+  infixl ` ⬝lmp `:75 := isomorphism.trans_eq
+  infixl ` ⬝plm `:75 := isomorphism.eq_trans
+
+  definition homomorphism_of_eq [constructor] {M₁ M₂ : LeftModule R} (p : M₁ = M₂ :> LeftModule R)
+    : M₁ →lm M₂ :=
+  isomorphism_of_eq p
+
+  definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
+  @is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
+
+  end
+
+end
+
+end left_module

algebra/module.hlean

@@ -1,86 +0,0 @@
-/-
-Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Nathaniel Thomas, Jeremy Avigad
-
-Modules prod vector spaces over a ring.
-
-(We use "left_module," which is more precise, because "module" is a keyword.)
--/
-import algebra.field
-open algebra
-
-structure has_scalar [class] (F V : Type) :=
-(smul : F → V → V)
-
-infixl ` • `:73 := has_scalar.smul
-
-/- modules over a ring -/
-
-structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming
-  mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
-  mul_left_inv→add_left_inv mul_comm→add_comm :=
-(smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
-(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add _ r s) x = (add (smul r x) (smul s x)))
-(mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x))
-(one_smul : Π x, smul one x = x)
-
-/- we make it a class now (and not as part of the structure) to avoid
-  left_module.to_ab_group to be an instance -/
-attribute left_module [class]
-
-definition add_ab_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
-  [H : left_module R M] : add_ab_group M :=
-@left_module.to_ab_group R M K H
-
-definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
-  [H : left_module R M] : has_scalar R M :=
-@left_module.to_has_scalar R M K H
-
-section left_module
-  variables {R M : Type}
-  variable  [ringR : ring R]
-  variable  [moduleRM : left_module R M]
-  include   ringR moduleRM
-
-  -- Note: the anonymous include does not work in the propositions below.
-
-  proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
-  !left_module.smul_left_distrib
-
-  proposition smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u :=
-  !left_module.smul_right_distrib
-
-  proposition mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
-  !left_module.mul_smul
-
-  proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul
-
-  proposition zero_smul (u : M) : (0 : R) • u = 0 :=
-  have (0 : R) • u + 0 • u = 0 • u + 0, by rewrite [-smul_right_distrib, *add_zero],
-  !add.left_cancel this
-
-  proposition smul_zero (a : R) : a • (0 : M) = 0 :=
-  have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
-  !add.left_cancel this
-
-  proposition neg_smul (a : R) (u : M) : (-a) • u = - (a • u) :=
-  eq_neg_of_add_eq_zero (by rewrite [-smul_right_distrib, add.left_inv, zero_smul])
-
-  proposition neg_one_smul (u : M) : -(1 : R) • u = -u :=
-  by rewrite [neg_smul, one_smul]
-
-  proposition smul_neg (a : R) (u : M) : a • (-u) = -(a • u) :=
-  by rewrite [-neg_one_smul, -mul_smul, mul_neg_one_eq_neg, neg_smul]
-
-  proposition smul_sub_left_distrib (a : R) (u v : M) : a • (u - v) = a • u - a • v :=
-  by rewrite [sub_eq_add_neg, smul_left_distrib, smul_neg]
-
-  proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v :=
-  by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul]
-end left_module
-
-/- vector spaces -/
-
-structure vector_space [class] (F V : Type) [fieldF : field F]
-  extends left_module F V

algebra/module_chain_complex.hlean

@@ -0,0 +1,57 @@
+/-
+Author: Jeremy Avigad
+-/
+import homotopy.chain_complex .left_module .is_short_exact ..move_to_lib
+open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc
+open algebra function
+open chain_complex
+open succ_str
+open left_module
+
+structure module_chain_complex (R : Ring) (N : succ_str) : Type :=
+(mod : N → LeftModule R)
+(hom : Π (n : N), left_module.homomorphism (mod (S n)) (mod n))
+(is_chain_complex :
+  Π (n : N) (x : mod (S (S n))), hom n (hom (S n) x) = 0)
+
+namespace module_chain_complex
+  variables {R : Ring} {N : succ_str}
+
+  definition mcc_mod [unfold 2] [coercion] (C : module_chain_complex R N) (n : N) :
+    LeftModule R :=
+  module_chain_complex.mod C n
+
+  definition mcc_carr [unfold 2] [coercion] (C : module_chain_complex R N) (n : N) :
+    Type :=
+  C n
+
+  definition mcc_pcarr [unfold 2] [coercion] (C : module_chain_complex R N) (n : N) :
+    Set* :=
+  mcc_mod C n
+
+  definition mcc_hom (C : module_chain_complex R N) {n : N} : C (S n) →lm C n :=
+  module_chain_complex.hom C n
+
+  definition mcc_is_chain_complex (C : module_chain_complex R N) (n : N) (x : C (S (S n))) :
+  mcc_hom C (mcc_hom C x) = 0 :=
+  module_chain_complex.is_chain_complex C n x
+
+  protected definition to_chain_complex [coercion] (C : module_chain_complex R N) :
+  chain_complex N :=
+    chain_complex.mk
+  (λ n, mcc_pcarr C n)
+  (λ n, pmap_of_homomorphism (@mcc_hom R N C n))
+  (mcc_is_chain_complex C)
+
+  -- maybe we don't even need this?
+  definition is_exact_at_m (C : module_chain_complex R N) (n : N) : Type :=
+  is_exact_at C n
+end module_chain_complex
+
+namespace left_module
+  variable  {R : Ring}
+  variables {A₀ B₀ C₀ : LeftModule R}
+  variables (f₀ : A₀ →lm B₀) (g₀ : B₀ →lm C₀)
+
+  definition is_short_exact := @_root_.is_short_exact  _ _ C₀ f₀ g₀
+end left_module

algebra/ses.hlean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Egbert Rijke. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Egbert Rijke
 
-Basic facts about short exact sequences. 
+Basic facts about short exact sequences.
 
 At the moment, it only covers short exact sequences of abelian groups, but this should be extended to short exact sequences in any abelian category.
 -/
@@ -13,18 +13,14 @@ import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .q
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
      equiv is_equiv
 
-structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
-  ( im_in_ker : Π(a:A), g (f a) = 1)
-  ( ker_in_im : Π(b:B), (g b = 1) → image_subgroup f b)
-
 structure SES (A B C : AbGroup) :=
   ( f : A →g B)
   ( g : B →g C)
   ( Hf : is_embedding f)
   ( Hg : is_surjective g)
-  ( ex : is_exact f g)
+  ( ex : is_exact_ag f g)
 
-definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) := 
+definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) :=
   begin
     have Hg : is_surjective (ab_qg_map (image_subgroup f)),
     from is_surjective_ab_qg_map (image_subgroup f),
@@ -37,7 +33,7 @@ definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f)
     intro a,
     fapply qg_map_eq_one, fapply tr, fapply fiber.mk, exact a, reflexivity,
     intro b, intro p,
-    fapply rel_of_ab_qg_map_eq_one, assumption
+    exact rel_of_ab_qg_map_eq_one _ p
   end
 
 definition SES_of_subgroup {B : AbGroup} (S : subgroup_rel B) : SES (ab_subgroup S) B (quotient_ab_group S) :=
@@ -73,7 +69,7 @@ definition SES_of_homomorphism {A B : AbGroup} (f : A →g B) : SES (ab_kernel f
     exact is_surjective_image_lift f,
     fapply is_exact.mk,
     intro a, induction a with a p, fapply subtype_eq, exact p,
-    intro a p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact a, 
+    intro a p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact a,
     exact calc
       f a = image_incl f (image_lift f a) : by exact homotopy_of_eq (ap group_fun (image_factor f)) a
       ... = image_incl f 1 : ap (image_incl f) p
@@ -90,10 +86,10 @@ definition SES_of_isomorphism_right {B C : AbGroup} (g : B ≃g C) : SES trivial
     fapply is_surjective_of_is_equiv,
     fapply is_exact.mk,
     intro a, induction a, fapply respect_one,
-    intro b p, 
+    intro b p,
     have q : g b = g 1,
-    from p ⬝ (respect_one g)⁻¹, 
-    note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q, 
+    from p ⬝ (respect_one g)⁻¹,
+    note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q,
     fapply tr, fapply fiber.mk, exact unit.star, rewrite r,
   end
 
@@ -134,6 +130,14 @@ begin
   krewrite [right_inv (equiv_of_isomorphism α) a], assumption
 end
 
+--definition quotient_SES {A B C : AbGroup} (ses : SES A B C) :
+--  quotient_ab_group (image_subgroup (SES.f ses)) ≃g C :=
+--  begin
+--    fapply ab_group_first_iso_thm B C (SES.g ses),
+--  end
+
+-- definition pre_right_extend_SES (to separate the following definition and replace C with B/A)
+
 definition quotient_codomain_SES : B_mod_A ≃g C :=
   begin
     exact (codomain_surjection_is_quotient g (SES.Hg ses))
@@ -150,7 +154,7 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
   (Σ (h : C →g C'), h ∘g g ~ k) ≃ (Σ (h' : B_mod_A →g C'), h' ∘g q ~ k) :=
   begin
     fapply equiv.mk,
-    intro pair, induction pair with h H, 
+    intro pair, induction pair with h H,
     fapply sigma.mk, exact h ∘g α, intro b,
     exact H b,
     fapply adjointify,
@@ -166,8 +170,8 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
     esimp, fapply is_prop.elimo, fapply pi.is_trunc_pi, intro a, fapply is_trunc_eq,
   end
 
-  parameters {A' B' C' : AbGroup} 
-  (ses' : SES A' B' C')  
+  parameters {A' B' C' : AbGroup}
+  (ses' : SES A' B' C')
   (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g f ~ (SES.f ses') ∘g hA)
 
   local abbreviation f' := SES.f ses'
@@ -175,12 +179,12 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
   local abbreviation ex' := SES.ex ses'
   local abbreviation q' := ab_qg_map (kernel_subgroup g')
   local abbreviation α' := quotient_codomain_SES
-  
+
   include htpy1
 
-  definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) := 
+  definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) :=
   begin
-    fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))), 
+    fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))),
     fapply ab_qg_universal_property,
     intro b, intro K,
     have k : trunctype.carrier (image_subgroup f b), from is_exact.ker_in_im ex b K,
@@ -211,7 +215,7 @@ definition quotient_extend_SES_square : k ∘g (ab_qg_map (kernel_subgroup g)) ~
     fapply quotient_group_compute
   end
 
-definition right_extend_SES  : C →g C' := 
+definition right_extend_SES  : C →g C' :=
   α' ∘g k ∘g α⁻¹ᵍ
 
 local abbreviation hC := right_extend_SES
@@ -242,7 +246,7 @@ definition right_extend_SES_unique_map (hC' : C →g C') (htpy2' : hC' ∘g g ~
   begin
     exact calc
       hC ~ α' ∘g k ∘g α⁻¹ᵍ : by reflexivity
-     ... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ : 
+     ... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ :
      ... ~ hC' ∘g α ∘g α⁻¹ᵍ : _
      ... ~ hC' : _
   end

algebra/short_five.hlean

@@ -0,0 +1,136 @@
+/-
+Author: Jeremy Avigad
+-/
+import .module_chain_complex
+open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc
+open algebra function succ_str
+open left_module
+
+section short_five
+  variable  {R : Ring}
+  variables {A₀ B₀ C₀ A₁ B₁ C₁ : LeftModule R}
+  variables {f₀ : A₀ →lm B₀} {g₀ : B₀ →lm C₀}
+  variables {f₁ : A₁ →lm B₁} {g₁ : B₁ →lm C₁}
+  variables {h  : A₀ →lm A₁} {k  : B₀ →lm B₁} {l  : C₀ →lm C₁}
+
+  premise   (short_exact₀ : is_short_exact f₀ g₀)
+  premise   (short_exact₁ : is_short_exact f₁ g₁)
+  premise   (hsquare₁ : hsquare f₀ f₁ h k)
+  premise   (hsquare₂ : hsquare g₀ g₁ k l)
+
+  include short_exact₀ short_exact₁ hsquare₁ hsquare₂
+
+  open is_short_exact
+
+  lemma short_five_mono [embh : is_embedding h] [embl : is_embedding l] :
+    is_embedding k :=
+  have is_embedding f₁, from is_emb short_exact₁,
+  is_embedding_of_is_add_hom k
+    (take b, suppose k b = 0,
+      have l (g₀ b) = 0, by rewrite [hsquare₂, ▸*, this, respect_zero],
+      have g₀ b = 0, from eq_zero_of_eq_zero_of_is_embedding this,
+      image.elim (ker_in_im short_exact₀ _ this)
+      (take a,
+        suppose f₀ a = b,
+        have f₁ (h a) = 0, by rewrite [-hsquare₁, ▸*, this]; assumption,
+        have h a = 0, from eq_zero_of_eq_zero_of_is_embedding this,
+        have a = 0, from eq_zero_of_eq_zero_of_is_embedding this,
+        show b = 0, by rewrite [-`f₀ a = b`, this, respect_zero]))
+
+  lemma short_five_epi (surjh : is_surjective h) (surjl : is_surjective l) :
+    is_surjective k :=
+  have surjg₀ : is_surjective g₀, from is_surj short_exact₀,
+  take b₁ : B₁,
+  image.elim (surjl (g₁ b₁)) (
+  take c₀ : C₀,
+  assume lc₀ : l c₀ = g₁ b₁,
+  image.elim (surjg₀ c₀) (
+  take b₀ : B₀,
+  assume g₀b₀ : g₀ b₀ = c₀,
+  have g₁ (k b₀ - b₁) = 0, by rewrite [respect_sub, -hsquare₂, ▸*, g₀b₀, lc₀, sub_self],
+  image.elim (ker_in_im short_exact₁ _ this) (
+  take a₁ : A₁,
+  assume f₁a₁ : f₁ a₁ = k b₀ - b₁,
+  image.elim (surjh a₁) (
+  take a₀ : A₀,
+  assume ha₀ : h a₀ = a₁,
+  have k (f₀ a₀) = k b₀ - b₁, by rewrite [hsquare₁, ▸*, ha₀, f₁a₁],
+  have k (b₀ - f₀ a₀) = b₁, by rewrite [respect_sub, this, sub_sub_self],
+  image.intro this))))
+end short_five
+
+section short_exact
+  open module_chain_complex
+  variables {R : Ring} {N : succ_str}
+
+  record is_short_exact_at (C : module_chain_complex R N) (n : N) :=
+  (is_contr_0 : is_contr (C n))
+  (is_exact_at_1 : is_exact_at_m C n)
+  (is_exact_at_2 : is_exact_at_m C (S n))
+  (is_exact_at_3 : is_exact_at_m C (S (S n)))
+  (is_contr_4 : is_contr (C (S (S (S (S n))))))
+
+  /- TODO: show that this gives rise to a short exact sequence in the sense above -/
+end short_exact
+
+section short_five_redux
+  open module_chain_complex
+  variables {R : Ring} {N : succ_str}
+
+  /- TODO: restate short five in these terms -/
+end short_five_redux
+
+
+/- TODO: state and prove strong_four, adapting the template below.
+
+section strong_four
+  variables {R : Type} [ring R]
+  variables {A B C D A' B' C' D' : Type}
+  variables [left_module R A] [left_module R B] [left_module R C] [left_module R D]
+  variables [left_module R A'] [left_module R B'] [left_module R C'] [left_module R D']
+
+  variables (ρ : A → B) [is_module_hom R ρ]
+  variables (σ : B → C) [is_module_hom R σ]
+  variables (τ : C → D) [is_module_hom R τ]
+  variable  (chainρσ : ∀ a, σ (ρ a) = 0)
+  variable  (exactρσ : ∀ {b}, σ b = 0 → ∃ a, ρ a = b)
+  variable  (chainστ : ∀ b, τ (σ b) = 0)
+  variable  (exactστ : ∀ {c}, τ c = 0 → ∃ b, σ b = c)
+
+  variables (ρ' : A' → B') [is_module_hom R ρ']
+  variables (σ' : B' → C') [is_module_hom R σ']
+  variables (τ' : C' → D') [is_module_hom R τ']
+  variable  (chainρ'σ' : ∀ a', σ' (ρ' a') = 0)
+  variable  (exactρ'σ' : ∀ {b'}, σ' b' = 0 → ∃ a', ρ' a' = b')
+  variable  (chainσ'τ' : ∀ b', τ' (σ' b') = 0)
+  variable  (exactσ'τ' : ∀ {c'}, τ' c' = 0 → ∃ b', σ' b' = c')
+
+  variables (α : A → A') [is_module_hom R α]
+  variables (β : B → B') [is_module_hom R β]
+  variables (γ : C → C') [is_module_hom R γ]
+  variables (δ : D → D') [is_module_hom R δ]
+
+  variables (sq₁ : comm_square ρ ρ' α β)
+  variables (sq₂ : comm_square σ σ' β γ)
+  variables (sq₃ : comm_square τ τ' γ δ)
+
+include sq₃ σ' sq₂ exactρ'σ' sq₁ chainρσ
+
+theorem strong_four_a (epiα : is_surjective α) (monoδ : is_embedding δ) (c : C) (γc0 : γ c = 0) :
+  Σ b, (β b = 0 × σ b = c) :=
+have δ (τ c) = 0, by rewrite [sq₃, γc0, hom_zero],
+have τ c = 0, from eq_zero_of_eq_zero_of_is_embedding this,
+obtain b (σbc : σ b = c), from exactστ this,
+have σ' (β b) = 0, by rewrite [-sq₂, σbc, γc0],
+obtain a' (ρ'a'βb : ρ' a' = β b), from exactρ'σ' this,
+obtain a (αaa' : α a = a'), from epiα a',
+exists.intro (b - ρ a)
+  (pair
+    (show β (b - ρ a) = 0, by rewrite [hom_sub, -ρ'a'βb, sq₁, αaa', sub_self])
+    (show σ (b - ρ a) = c, from calc
+       σ (b - ρ a) = σ b - σ (ρ a) : hom_sub _
+               ... = σ b           : by rewrite [chainρσ, sub_zero]
+               ... = c             : σbc))
+
+end strong_four
+-/

colim.hlean

@@ -363,7 +363,7 @@ namespace seq_colim
     (q : prep0 f n (Point (A 0)) = Point (A n))
     : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
     (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
-  by rewrite [▸*, con_inv, +ap_con, ap_inv, +con.assoc]
+  by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
 
   definition succ_add_tr_rep {n : ℕ} (k : ℕ) (x : A n)
     : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x :=

homotopy/cohomology.hlean

@@ -11,18 +11,6 @@ import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_l
 open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
      function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi
 
--- TODO: move
-structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
-  ( im_in_ker : Π(a:A), g (f a) = pt)
-  ( ker_in_im : Π(b:B), (g b = pt) → image f b)
-
-definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
-is_exact f g
-
-definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
-  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
-is_exact.mk H₁ H₂
-
 definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
   (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
 begin
@@ -49,8 +37,8 @@ definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
 begin
   fconstructor,
   { intro p, esimp,
-    refine ap1_gen_con_left p (respect_pt f) (respect_pt f)
-             (respect_pt g) (respect_pt g) ⬝ _,
+    refine ap1_gen_con_left (respect_pt f) (respect_pt f)
+             (respect_pt g) (respect_pt g) p ⬝ _,
     refine !whisker_right_idp ◾ !whisker_left_idp2, },
   { refine !con.assoc ⬝ _,
     refine _ ◾ idp ⬝ _, rotate 1,

homotopy/pushout.hlean

@@ -464,10 +464,6 @@ namespace pushout
 
   /- universal property of cofiber -/
 
-  structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
-  ( im_in_ker : Π(a:A), g (f a) = pt)
-  ( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
-
   definition cofiber_exact_1 {X Y Z : Type*} (f : X →* Y) (g : pcofiber f →* Z) :
     (g ∘* pcod f) ∘* f ~* pconst X Z :=
   !passoc ⬝* pwhisker_left _ !pcod_pcompose ⬝* !pcompose_pconst

homotopy/smash.hlean

@@ -306,6 +306,17 @@ namespace smash
   !smash_functor_phomotopy_trans⁻¹ ⬝ ap011 smash_functor_phomotopy p q ⬝
   !smash_functor_phomotopy_trans
 
+  definition smash_functor_eq_of_phomotopy (f : A →* C) {g g' : B →* D}
+    (p : g ~* g') : ap (smash_functor f) (eq_of_phomotopy p) =
+    eq_of_phomotopy (smash_functor_phomotopy phomotopy.rfl p) :=
+  begin
+    induction p using phomotopy_rec_on_idp,
+    refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
+    refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
+    apply ap eq_of_phomotopy,
+    exact !smash_functor_phomotopy_refl⁻¹
+  end
+
   /- the functorial action preserves compositions, the interchange law -/
   definition smash_functor_pcompose_homotopy [unfold 11] {C D E F : Type}
     (f' : C → E) (f : A → C) (g' : D → F) (g : B → D) :
@@ -336,6 +347,10 @@ namespace smash
     { reflexivity }
   end
 
+  definition smash_functor_split (f : A →* C) (g : B →* D) :
+    f ∧→ g ~* (pid C) ∧→ g ∘* f ∧→ (pid B)  :=
+  smash_functor_phomotopy !pid_pcompose⁻¹* !pcompose_pid⁻¹* ⬝* !smash_functor_pcompose
+
   /- An alternative proof which doesn't start by applying inductions, so which is more explicit -/
   -- definition smash_functor_pcompose_homotopy [unfold 11] (f' : C →* E) (f : A →* C) (g' : D →* F)
   --   (g : B →* D) : (f' ∘* f) ∧→ (g' ∘* g) ~ (f' ∧→ g') ∘* (f ∧→ g) :=
@@ -446,10 +461,18 @@ namespace smash
     exact !smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans
   end
 
-  /- We need two coherence rules for the naturality of the smash-pmap adjunction. Given the function
-     h := (f' ∘ f) ∧→ (g' ∘ g) and suppose that either g' or g is constant. There are two ways to
-     show that h is constant: either by using exchange, or directly. We need to show that these two
-     proofs result in the same pointed homotopy. First we do the case where g is constant -/
+  /- This makes smash_functor into a pointed map (B →* B') →* (A ∧ B →* A ∧ B') -/
+
+  definition smash_functor_right [constructor] (A B C : Type*) :
+    ppmap B C →* ppmap (A ∧ B) (A ∧ C) :=
+  pmap.mk (smash_functor (pid A)) (eq_of_phomotopy (smash_functor_pconst_right (pid A)))
+
+  /- We want to show that smash_functor_right is natural in A, B and C.
+
+     For this we need two coherence rules. Given the function h := (f' ∘ f) ∧→ (g' ∘ g) and suppose
+     that either g' or g is constant. There are two ways to show that h is constant: either by using
+     exchange, or directly. We need to show that these two proofs result in the same pointed
+     homotopy. First we do the case where g is constant -/
 
   private definition my_squarel {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₂ = a₃) :
     square (p₁ ⬝ p₂⁻¹) p₂⁻¹ p₁ idp :=
@@ -487,7 +510,7 @@ namespace smash
     idp
     (smash_functor_pconst_right_homotopy (λ a, f' (f a)) x)
     (ap (smash_functor' (pmap.mk f' (refl (f' (f a₀)))) (pmap.mk g (refl (g d₀))))
-       (smash_functor_pconst_right_homotopy f x)) :=
+      (smash_functor_pconst_right_homotopy f x)) :=
   begin
     induction x with a b a b,
     { refine _ ⬝hp (functor_gluel'2 f' g (f a) (f a₀))⁻¹, exact hrfl },
@@ -548,10 +571,8 @@ namespace smash
              (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g))
              (pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝*
                pcompose_pconst (pid A ∧→ g)) :=
-  begin
-    refine (_ ◾** idp ⬝ !refl_trans) ⬝pv** smash_functor_pcompose_pconst (pid A) (pid A) g,
-    apply smash_functor_phomotopy_refl,
-  end
+  (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
+  smash_functor_pcompose_pconst (pid A) (pid A) g
 
   /- a small rewrite of the previous -/
   definition smash_functor_pid_pcompose_pconst' (g : D →* F) :
@@ -633,40 +654,63 @@ namespace smash
       rexact H (gluel (f' (f a₀))) }
   end
 
-  /- a lemma using both these rules -/
+  /- a version where the left maps are identities -/
+  definition smash_functor_pid_pconst_pcompose (g : B →* D) :
+    phsquare (smash_functor_pid_pcompose A (pconst D F) g)
+             (smash_functor_pconst_right (pid A))
+             (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose g))
+             (pwhisker_right (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝*
+               pconst_pcompose (pid A ∧→ g)) :=
+  (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
+  smash_functor_pconst_pcompose (pid A) (pid A) g
 
-  definition smash_psquare_lemma (f : A →* A') (g : B →* B')
-    : phsquare (smash_functor_psquare (pvrefl g) (pid_pcompose (pconst A' C ∘* f))⁻¹*)
-               (pconst_pcompose (g ∧→ f))
-               (pwhisker_right (g ∧→ f) (smash_functor_pconst_right (pid B')))
-               (pwhisker_left (g ∧→ pid C)
-                   (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose f) ⬝*
-                    smash_functor_pconst_right (pid B)) ⬝*
-                 pcompose_pconst (g ∧→ pid C)) :=
+  /- these lemmas are use to show that smash_functor_right is natural in all arguments -/
+  definition smash_functor_right_natural_right (f : C →* C') :
+    psquare (smash_functor_right A B C) (smash_functor_right A B C')
+            (ppcompose_left f) (ppcompose_left (pid A ∧→ f)) :=
   begin
-    refine !trans_assoc ⬝pv** _,
-    apply phmove_top_of_left',
-    refine _ ⬝ (!trans_assoc ⬝ !smash_functor_pconst_pcompose)⁻¹,
-    refine !trans_assoc⁻¹ ⬝ trans_eq_of_eq_trans_symm _,
-    refine _ ⬝hp** !pwhisker_left_trans⁻¹,
-    refine (smash_functor_phomotopy_phsquare (phvrfl ⬝hp** !pcompose2_refl⁻¹)
-      (!pcompose2_refl_left ⬝ph** !pid_pconst_pcompose)⁻¹ʰ** ⬝h**
-      !smash_functor_pcompose_phomotopy ⬝hp**
-      (!smash_functor_phomotopy_refl ◽* idp ⬝ !pcompose2_refl_left)) ⬝v** _,
-    refine ((!smash_functor_phomotopy_trans⁻¹ ⬝
-      ap011 smash_functor_phomotopy !trans_refl !refl_trans) ◾** idp) ⬝ph** idp ⬝ _,
-    refine !trans_assoc ⬝ !trans_assoc ⬝ _,
-    apply trans_eq_of_eq_symm_trans,
-    refine _ ⬝ !trans_assoc ⬝ (ap (smash_functor_phomotopy _) !refl_symm⁻¹ ⬝
-      !smash_functor_phomotopy_symm) ◾** idp,
-    refine _ ⬝ !smash_functor_pconst_right_phomotopy⁻¹ ◾** idp,
-    apply trans_eq_of_eq_symm_trans,
-    refine _ ⬝ !trans_assoc ⬝ (ap011 smash_functor_phomotopy !refl_symm⁻¹ !refl_symm⁻¹ ⬝
-      !smash_functor_phomotopy_symm) ◾** idp,
-    apply eq_trans_symm_of_trans_eq, refine !trans_assoc ⬝ _,
-    apply smash_functor_pcompose_pconst
+    refine _⁻¹*,
+    fapply phomotopy_mk_ppmap,
+    { exact smash_functor_pid_pcompose A f },
+    { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
+      refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply smash_functor_pid_pcompose_pconst }
   end
 
+  definition smash_functor_right_natural_middle (f : B' →* B) :
+    psquare (smash_functor_right A B C) (smash_functor_right A B' C)
+            (ppcompose_right f) (ppcompose_right (pid A ∧→ f)) :=
+  begin
+    refine _⁻¹*,
+    fapply phomotopy_mk_ppmap,
+    { intro g, exact smash_functor_pid_pcompose A g f },
+    { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
+      refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply smash_functor_pid_pconst_pcompose }
+  end
+
+  definition smash_functor_right_natural_left (f : A →* A') :
+    psquare (smash_functor_right A B C) (ppcompose_right (f ∧→ (pid B)))
+            (smash_functor_right A' B C) (ppcompose_left (f ∧→ (pid C))) :=
+  begin
+    refine _⁻¹*,
+    fapply phomotopy_mk_ppmap,
+    { intro g, exact smash_functor_psquare proof phomotopy.rfl qed proof phomotopy.rfl qed },
+    { esimp,
+      refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
+      refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply eq_of_phsquare,
+      refine (phmove_bot_of_left _ !smash_functor_pconst_pcompose⁻¹ʰ**) ⬝h**
+        (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst ⬝vp** _,
+      refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl,
+      refine idp ◾** !refl_trans ⬝ !trans_left_inv }
+  end
 
   /- f ∧ g is a pointed equivalence if f and g are -/
   definition smash_functor_using_pushout [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D :=
@@ -692,18 +736,18 @@ namespace smash
   end
 
   local attribute is_equiv_sum_functor [instance]
-  definition smash_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D :=
+  definition smash_pequiv [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D :=
   begin
     fapply pequiv_of_pmap (f ∧→ g),
     refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ,
     apply pushout.is_equiv_functor
   end
 
-  definition smash_pequiv_smash_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B :=
-  smash_pequiv_smash f pequiv.rfl
+  definition smash_pequiv_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B :=
+  smash_pequiv f pequiv.rfl
 
-  definition smash_pequiv_smash_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
-  smash_pequiv_smash pequiv.rfl g
+  definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
+  smash_pequiv pequiv.rfl g
 
   /- A ∧ B ≃* pcofiber (pprod_of_pwedge A B) -/
 

homotopy/smash_adjoint.hlean

@@ -2,11 +2,10 @@
 -- in collaboration with Egbert, Stefano, Robin, Ulrik
 
 /- the adjunction between the smash product and pointed maps -/
-import .smash
+import .smash .susp
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
-     function red_susp unit sigma
-
+     function unit sigma susp sphere
 
 namespace smash
 
@@ -121,7 +120,7 @@ namespace smash
   end
 
   /- The counit is natural in both arguments -/
-  definition smash_pmap_counit_natural (g : B →* C) : g ∘* smash_pmap_counit A B ~*
+  definition smash_pmap_counit_natural_right (g : B →* C) : g ∘* smash_pmap_counit A B ~*
     smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) :=
   begin
     symmetry,
@@ -214,7 +213,7 @@ namespace smash
       refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹,
       refine _ ⬝ !trans_refl⁻¹,
       fapply phomotopy_eq,
-      { intro a, refine !elim_gluel'⁻¹ },
+      { intro a, esimp, refine !elim_gluel'⁻¹ },
       { esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹,
         refine whisker_right _ !elim_gluel'_same⁻² ⬝ _ ⬝ !elim_gluer'_same⁻¹⁻²,
         apply inv_con_eq_of_eq_con, refine !idp_con ⬝ _, esimp,
@@ -245,7 +244,7 @@ namespace smash
   begin
     refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _,
     refine !passoc⁻¹* ⬝* _,
-    refine !pwhisker_right !smash_pmap_counit_natural⁻¹* ⬝* _,
+    refine !pwhisker_right !smash_pmap_counit_natural_right⁻¹* ⬝* _,
     refine !passoc ⬝* _,
     refine !pwhisker_left !smash_pmap_unit_counit ⬝* _,
     apply pcompose_pid
@@ -268,15 +267,15 @@ namespace smash
       apply pconst_pcompose_phomotopy_pconst }
   end
 
-  definition smash_elim_natural {A B C C' : Type*} (f : C →* C')
+  definition smash_elim_natural_right {A B C C' : Type*} (f : C →* C')
     (g : B →* ppmap A C) : f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) :=
   begin
     refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
     refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
-    apply smash_pmap_counit_natural
+    apply smash_pmap_counit_natural_right
   end
 
-  definition smash_elim_inv_natural {A B C C' : Type*} (f : C →* C')
+  definition smash_elim_inv_natural_right {A B C C' : Type*} (f : C →* C')
     (g : A ∧ B →* C) : ppcompose_left f ∘* smash_elim_inv g ~* smash_elim_inv (f ∘* g) :=
   begin
     refine !passoc⁻¹* ⬝* pwhisker_right _ _,
@@ -326,86 +325,42 @@ namespace smash
 
   /- The pointed maps of the equivalence A →* (B →* C) ≃* A ∧ B →* C -/
   definition smash_pelim [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C :=
-  pmap.mk smash_elim (eq_of_phomotopy !smash_elim_pconst)
+  ppcompose_left (smash_pmap_counit B C) ∘* smash_functor_right B A (ppmap B C)
 
   definition smash_pelim_inv [constructor] (A B C : Type*) :
     ppmap (B ∧ A) C →* ppmap A (ppmap B C) :=
   pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst)
 
   /- The forward function is natural in all three arguments -/
-  theorem smash_elim_natural_pconst (f : C →* C') :
-    smash_elim_natural f (pconst A (ppmap B C)) ⬝*
-   (smash_elim_phomotopy (pcompose_pconst (ppcompose_left f)) ⬝*
-    smash_elim_pconst B A C') =
-    pwhisker_left f (smash_elim_pconst B A C) ⬝*
-    pcompose_pconst f :=
-  begin
-    refine idp ◾** (!trans_assoc⁻¹ ⬝ (!pwhisker_left_trans⁻¹ ◾** idp)) ⬝ _,
-    refine !trans_assoc⁻¹ ⬝ _,
-    refine (!trans_assoc ⬝ (idp ◾** (!pwhisker_left_trans⁻¹ ⬝
-      ap (pwhisker_left _) (smash_functor_pid_pcompose_pconst' (ppcompose_left f))⁻¹ ⬝
-      !pwhisker_left_trans))) ◾** idp ⬝ _,
-    refine (!trans_assoc⁻¹ ⬝ (!passoc_phomotopy_right⁻¹ʰ** ⬝h**
-      !pwhisker_right_pwhisker_left ⬝h** !passoc_phomotopy_right) ◾** idp) ◾** idp ⬝ _,
-    refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾**_ ⬝ !trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp,
-    refine !trans_assoc ⬝ !trans_assoc ⬝ (eq_symm_trans_of_trans_eq _)⁻¹,
-    refine !passoc_pconst_right ⬝ _,
-    refine _ ⬝ idp ◾** !passoc_pconst_right⁻¹,
-    refine !pcompose_pconst_phomotopy⁻¹
-  end
+  definition smash_pelim_natural_right (f : C →* C') :
+    psquare (smash_pelim A B C) (smash_pelim A B C')
+            (ppcompose_left (ppcompose_left f)) (ppcompose_left f) :=
+  smash_functor_right_natural_right (ppcompose_left f) ⬝h*
+  ppcompose_left_psquare (smash_pmap_counit_natural_right f)
 
-  definition smash_pelim_natural (f : C →* C') :
-    ppcompose_left f ∘* smash_pelim A B C ~*
-    smash_pelim A B C' ∘* ppcompose_left (ppcompose_left f) :=
-  begin
-    fapply phomotopy_mk_ppmap,
-    { exact smash_elim_natural f },
-    { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_eq_of_phomotopy ⬝
-        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
-      refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝
-        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
-      exact smash_elim_natural_pconst f }
-  end
+  definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) :
+    psquare (smash_pelim A B C) (smash_pelim A' B C)
+            (ppcompose_right f) (ppcompose_right (pid B ∧→ f)) :=
+  smash_functor_right_natural_middle f ⬝h* !ppcompose_left_ppcompose_right
 
-  definition smash_pelim_natural_left (C : Type*) (f : A →* A') (g : B →* B') :
-    psquare (smash_pelim A' B' C) (smash_pelim A B C)
+  definition smash_pelim_natural_middle (A C : Type*) (g : B' →* B) :
+    psquare (smash_pelim A B C) (smash_pelim A B' C)
+            (ppcompose_left (ppcompose_right g)) (ppcompose_right (g ∧→ pid A)) :=
+  pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝*
+  (!smash_functor_right_natural_left⁻¹* ⬝pv*
+  smash_functor_right_natural_right (ppcompose_right g) ⬝h*
+  ppcompose_left_psquare !smash_pmap_counit_natural_left)
+
+  definition smash_pelim_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) :
+    psquare (smash_pelim A B C) (smash_pelim A' B' C)
             (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (g ∧→ f)) :=
-  begin
-    fapply phomotopy_mk_ppmap,
-    { intro h, apply smash_elim_natural_left },
-    { esimp,
-      refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq
-        (ap02 _ (whisker_right _ !pcompose_left_eq_of_phomotopy ⬝ !eq_of_phomotopy_trans⁻¹) ⬝
-        !smash_elim_eq_of_phomotopy) ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
-        !phomotopy_of_eq_of_phomotopy) ⬝ _,
-      refine _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ idp ⬝
-        !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹,
-      refine ((idp ⬝h** ((ap (pwhisker_left _) (!trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp) ⬝
-        !pwhisker_left_trans)⁻¹ ⬝ph** (pwhisker_left_phsquare _
-        (!smash_functor_phomotopy_trans_right ⬝ph**
-        (!smash_functor_pid_pcompose_phomotopy_right ⬝v**
-        !smash_functor_pid_pcompose_pconst))⁻¹ʰ** ⬝vp** !pwhisker_left_symm))) ⬝v**
-        (phwhisker_rt _ idp)) ⬝ _,
-      refine (idp ⬝h** (!passoc_phomotopy_right ⬝v** idp)) ◾** idp ⬝ _,
-      refine !trans_assoc ⬝ idp ◾** (!trans_assoc ⬝ !trans_assoc ⬝ idp ◾**
-        !passoc_pconst_right) ⬝ _,
-      refine idp ⬝h** (phwhisker_br _ !pwhisker_right_pwhisker_left ⬝vp**
-        !pcompose_pconst_phomotopy) ⬝ _,
-      refine (idp ⬝h** (phwhisker_br _ !passoc_phomotopy_right⁻¹ʰ** ⬝vp**
-        (eq_symm_trans_of_trans_eq !passoc_pconst_right)⁻¹)) ⬝ _,
-      refine (idp ⬝h** ((idp ◾** !pwhisker_left_trans⁻¹ ⬝
-        pwhisker_left_phsquare _ !smash_psquare_lemma) ⬝v** idp ⬝hp** !trans_assoc)) ⬝ _,
-      refine (!passoc_phomotopy_middle ⬝v** idp ⬝v** idp) ⬝ _,
-      refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** !passoc_pconst_middle ⬝ _,
-      refine !trans_assoc⁻¹ ⬝ _ ◾** idp,
-      exact !pwhisker_right_trans⁻¹ }
-  end
+  smash_pelim_natural_left B C f ⬝v* smash_pelim_natural_middle A' C g ⬝hp*
+  ppcompose_right_phomotopy proof !smash_functor_split qed ⬝* !ppcompose_right_pcompose
 
   /- The equivalence (note: the forward function of smash_adjoint_pmap is smash_pelim_inv) -/
-  definition smash_adjoint_pmap' [constructor] (A B C : Type*) : B →* ppmap A C ≃ A ∧ B →* C :=
+  definition is_equiv_smash_elim [constructor] (A B C : Type*) : is_equiv (@smash_elim A B C) :=
   begin
-    fapply equiv.MK,
-    { exact smash_elim },
+    fapply adjointify,
     { exact smash_elim_inv },
     { intro g, apply eq_of_phomotopy, exact smash_elim_right_inv g },
     { intro f, apply eq_of_phomotopy, exact smash_elim_left_inv f }
@@ -413,43 +368,43 @@ namespace smash
 
   definition smash_adjoint_pmap_inv [constructor] (A B C : Type*) :
     ppmap B (ppmap A C) ≃* ppmap (A ∧ B) C :=
-  pequiv_of_equiv (smash_adjoint_pmap' A B C) (eq_of_phomotopy (smash_elim_pconst A B C))
+  pequiv_of_pmap (smash_pelim B A C) (is_equiv_smash_elim B A C)
 
   definition smash_adjoint_pmap [constructor] (A B C : Type*) :
     ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) :=
   (smash_adjoint_pmap_inv A B C)⁻¹ᵉ*
 
   /- The naturality of the equivalence is a direct consequence of the earlier naturalities -/
-  definition smash_adjoint_pmap_natural_pt {A B C C' : Type*} (f : C →* C') (g : A ∧ B →* C) :
+  definition smash_adjoint_pmap_natural_right_pt {A B C C' : Type*} (f : C →* C') (g : A ∧ B →* C) :
     ppcompose_left f ∘* smash_adjoint_pmap A B C g ~* smash_adjoint_pmap A B C' (f ∘* g) :=
   begin
     refine !passoc⁻¹* ⬝* pwhisker_right _ _,
     exact !ppcompose_left_pcompose⁻¹*
   end
 
-  definition smash_adjoint_pmap_inv_natural_pt {A B C C' : Type*} (f : C →* C')
+  definition smash_adjoint_pmap_inv_natural_right_pt {A B C C' : Type*} (f : C →* C')
     (g : B →* ppmap A C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~*
     (smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) :=
   begin
     refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
     refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
-    apply smash_pmap_counit_natural
+    apply smash_pmap_counit_natural_right
   end
 
-  definition smash_adjoint_pmap_inv_natural [constructor] {A B C C' : Type*} (f : C →* C') :
+   definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
     ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~*
     smash_adjoint_pmap_inv A B C' ∘* ppcompose_left (ppcompose_left f) :=
-  smash_pelim_natural f
+  smash_pelim_natural_right f
 
-  definition smash_adjoint_pmap_natural [constructor] {A B C C' : Type*} (f : C →* C') :
+  definition smash_adjoint_pmap_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
     ppcompose_left (ppcompose_left f) ∘* smash_adjoint_pmap A B C ~*
     smash_adjoint_pmap A B C' ∘* ppcompose_left f :=
-  (smash_adjoint_pmap_inv_natural f)⁻¹ʰ*
+  (smash_adjoint_pmap_inv_natural_right f)⁻¹ʰ*
 
-  definition smash_adjoint_pmap_natural_left (C : Type*) (f : A →* A') (g : B →* B') :
+  definition smash_adjoint_pmap_natural_lm (C : Type*) (f : A →* A') (g : B →* B') :
     psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C)
             (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right f) ∘* ppcompose_right g) :=
-  (smash_pelim_natural_left C g f)⁻¹ʰ*
+  (smash_pelim_natural_lm C g f)⁻¹ʰ*
 
   /- Corollary: associativity of smash -/
 
@@ -465,49 +420,50 @@ namespace smash
     (A ∧ B) ∧ C →* X :=
   smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f)))
 
-  definition smash_assoc_elim_natural (A B C : Type*) (f : X →* X') :
+  definition smash_assoc_elim_natural_right (A B C : Type*) (f : X →* X') :
     psquare (smash_assoc_elim_equiv A B C X) (smash_assoc_elim_equiv A B C X')
             (ppcompose_left f) (ppcompose_left f) :=
-  !smash_adjoint_pmap_natural ⬝h*
-  !smash_adjoint_pmap_natural ⬝h*
-  ppcompose_left_psquare !smash_adjoint_pmap_inv_natural ⬝h*
-  !smash_adjoint_pmap_inv_natural
+  !smash_adjoint_pmap_natural_right ⬝h*
+  !smash_adjoint_pmap_natural_right ⬝h*
+  ppcompose_left_psquare !smash_adjoint_pmap_inv_natural_right ⬝h*
+  !smash_adjoint_pmap_inv_natural_right
 
   /-
-    We could prove the following two pointed homotopies by applying smash_assoc_elim_natural to g,
-    but we give a more explicit proof
+    We could prove the following two pointed homotopies by applying smash_assoc_elim_natural_right
+    to g, but we give a more explicit proof
   -/
-  definition smash_assoc_elim_natural_pt {A B C X X' : Type*} (f : X →* X') (g : A ∧ (B ∧ C) →* X) :
+  definition smash_assoc_elim_natural_right_pt {A B C X X' : Type*} (f : X →* X')
+    (g : A ∧ (B ∧ C) →* X) :
     f ∘* smash_assoc_elim_equiv A B C X g ~* smash_assoc_elim_equiv A B C X' (f ∘* g) :=
   begin
-    refine !smash_adjoint_pmap_inv_natural_pt ⬝* _,
+    refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _,
     apply smash_elim_phomotopy,
     refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ !smash_adjoint_pmap_inv_natural ⬝* _,
+    refine pwhisker_right _ !smash_adjoint_pmap_inv_natural_right ⬝* _,
     refine !passoc ⬝* _,
     apply pwhisker_left,
-    refine !smash_adjoint_pmap_natural_pt ⬝* _,
+    refine !smash_adjoint_pmap_natural_right_pt ⬝* _,
     apply smash_elim_inv_phomotopy,
-    refine !smash_adjoint_pmap_natural_pt
+    refine !smash_adjoint_pmap_natural_right_pt
   end
 
-  definition smash_assoc_elim_inv_natural_pt {A B C X X' : Type*} (f : X →* X')
+  definition smash_assoc_elim_inv_natural_right_pt {A B C X X' : Type*} (f : X →* X')
     (g : (A ∧ B) ∧ C →* X) :
     f ∘* (smash_assoc_elim_equiv A B C X)⁻¹ᵉ* g ~* (smash_assoc_elim_equiv A B C X')⁻¹ᵉ* (f ∘* g) :=
   begin
-    refine !smash_adjoint_pmap_inv_natural_pt ⬝* _,
+    refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _,
     apply smash_elim_phomotopy,
     refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ !smash_pmap_counit_natural ⬝* _,
+    refine pwhisker_right _ !smash_pmap_counit_natural_right ⬝* _,
     refine !passoc ⬝* _,
     apply pwhisker_left,
     refine !smash_functor_pid_pcompose⁻¹* ⬝* _,
     apply smash_functor_phomotopy phomotopy.rfl,
     refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ !smash_adjoint_pmap_natural ⬝* _,
+    refine pwhisker_right _ !smash_adjoint_pmap_natural_right ⬝* _,
     refine !passoc ⬝* _,
     apply pwhisker_left,
-    apply smash_elim_inv_natural
+    apply smash_elim_inv_natural_right
   end
 
   definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
@@ -515,37 +471,108 @@ namespace smash
     fapply pequiv.MK2,
     { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid },
     { exact !smash_assoc_elim_equiv !pid },
-    { refine !smash_assoc_elim_inv_natural_pt ⬝* _,
+    { refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
       refine pap !smash_assoc_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
       apply phomotopy_of_eq, apply to_left_inv !smash_assoc_elim_equiv },
-    { refine !smash_assoc_elim_natural_pt ⬝* _,
+    { refine !smash_assoc_elim_natural_right_pt ⬝* _,
       refine pap !smash_assoc_elim_equiv !pcompose_pid ⬝* _,
       apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv }
   end
 
   /- the associativity of smash is natural in all arguments -/
-  definition smash_assoc_elim_equiv_natural_left (X : Type*)
+  definition smash_assoc_elim_natural_left (X : Type*)
     (f : A →* A') (g : B →* B') (h : C →* C') :
     psquare (smash_assoc_elim_equiv A' B' C' X) (smash_assoc_elim_equiv A B C X)
             (ppcompose_right (f ∧→ g ∧→ h)) (ppcompose_right ((f ∧→ g) ∧→ h)) :=
   begin
-    refine !smash_adjoint_pmap_natural_left ⬝h* _ ⬝h*
-      (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_pelim_natural_left) ⬝h*
-      !smash_pelim_natural_left,
+    refine !smash_adjoint_pmap_natural_lm ⬝h* _ ⬝h*
+      (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_pelim_natural_lm) ⬝h*
+      !smash_pelim_natural_lm,
     refine !ppcompose_left_ppcompose_right⁻¹* ⬝ph* _,
     refine _ ⬝hp* pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝*
       !ppcompose_left_pcompose) ⬝* !passoc ⬝* pwhisker_left _ !ppcompose_left_ppcompose_right⁻¹* ⬝*
       !passoc⁻¹*,
-    refine _ ⬝v* !smash_adjoint_pmap_natural_left,
-    refine !smash_adjoint_pmap_natural
+    refine _ ⬝v* !smash_adjoint_pmap_natural_lm,
+    refine !smash_adjoint_pmap_natural_right
   end
 
   definition smash_assoc_natural (f : A →* A') (g : B →* B') (h : C →* C') :
     psquare (smash_assoc A B C) (smash_assoc A' B' C') (f ∧→ (g ∧→ h)) ((f ∧→ g) ∧→ h) :=
   begin
-    refine !smash_assoc_elim_inv_natural_pt ⬝* _,
+    refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
     refine pap !smash_assoc_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
-    rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
+    rexact phomotopy_of_eq ((smash_assoc_elim_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
   end
 
+  /- Corollary 2: smashing with a suspension -/
+  definition smash_psusp_elim_equiv (A B X : Type*) :
+    ppmap (A ∧ psusp B) X ≃* ppmap (psusp (A ∧ B)) X :=
+  calc
+    ppmap (A ∧ psusp B) X ≃* ppmap (psusp B) (ppmap A X) : smash_adjoint_pmap A (psusp B) X
+    ... ≃* ppmap B (Ω (ppmap A X)) : psusp_adjoint_loop' B (ppmap A X)
+    ... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_pmap_commute A X)
+    ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
+    ... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X
+
+  definition smash_psusp_elim_natural_right (A B : Type*) (f : X →* X') :
+    psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A B X')
+            (ppcompose_left f) (ppcompose_left f) :=
+  smash_adjoint_pmap_natural_right f ⬝h*
+  psusp_adjoint_loop_natural_right (ppcompose_left f) ⬝h*
+  ppcompose_left_psquare (loop_pmap_commute_natural_right A f) ⬝h*
+  (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h*
+  (psusp_adjoint_loop_natural_right f)⁻¹ʰ*
+
+  definition smash_psusp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) :
+    psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A' B' X)
+            (ppcompose_right (f ∧→ psusp_functor g)) (ppcompose_right (psusp_functor (f ∧→ g))) :=
+  begin
+    refine smash_adjoint_pmap_natural_lm X f (psusp_functor g) ⬝h*
+           _ ⬝h* _ ⬝h*
+           (smash_adjoint_pmap_natural_lm (Ω X) f g)⁻¹ʰ* ⬝h*
+           (psusp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*,
+    rotate 2,
+    exact !ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare (loop_pmap_commute_natural_left X f),
+    exact psusp_adjoint_loop_natural_left g ⬝v* psusp_adjoint_loop_natural_right (ppcompose_right f)
+  end
+
+  definition smash_psusp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) :=
+  begin
+    fapply pequiv.MK2,
+    { exact !smash_psusp_elim_equiv⁻¹ᵉ* !pid },
+    { exact !smash_psusp_elim_equiv !pid },
+    { refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
+      refine pap !smash_psusp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
+      apply phomotopy_of_eq, apply to_left_inv !smash_psusp_elim_equiv },
+    { refine phomotopy_of_eq (!smash_psusp_elim_natural_right _) ⬝* _,
+      refine pap !smash_psusp_elim_equiv !pcompose_pid ⬝* _,
+      apply phomotopy_of_eq, apply to_right_inv !smash_psusp_elim_equiv }
+  end
+
+  definition smash_psusp_natural (f : A →* A') (g : B →* B') :
+    psquare (smash_psusp A B) (smash_psusp A' B') (f ∧→ (psusp_functor g)) (psusp_functor (f ∧→ g)) :=
+  begin
+    refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
+    refine pap !smash_psusp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
+    rexact phomotopy_of_eq ((smash_psusp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹
+  end
+
+  definition smash_iterate_psusp (n : ℕ) (A B : Type*) : A ∧ iterate_psusp n B ≃* iterate_psusp n (A ∧ B) :=
+  begin
+    induction n with n e,
+    { reflexivity },
+    { exact smash_psusp A (iterate_psusp n B) ⬝e* psusp_pequiv e }
+  end
+
+  definition smash_sphere (A : Type*) (n : ℕ) : A ∧ psphere n ≃* iterate_psusp n A :=
+  smash_pequiv pequiv.rfl (psphere_pequiv_iterate_psusp n) ⬝e*
+  smash_iterate_psusp n A pbool ⬝e*
+  iterate_psusp_pequiv n (smash_pbool_pequiv A)
+
+  definition sphere_smash_sphere (n m : ℕ) : psphere n ∧ psphere m ≃* psphere (n+m) :=
+  smash_sphere (psphere n) m ⬝e*
+  iterate_psusp_pequiv m (psphere_pequiv_iterate_psusp n) ⬝e*
+  iterate_psusp_iterate_psusp_rev m n pbool ⬝e*
+  (psphere_pequiv_iterate_psusp (n + m))⁻¹ᵉ*
+
 end smash

homotopy/spherical_fibrations.hlean

@@ -59,7 +59,7 @@ namespace spherical_fibrations
   begin
     intro X, cases X with X p,
     apply sigma.mk (psusp X), induction p with f, apply tr,
-    apply susp.psusp_equiv f
+    apply susp.psusp_pequiv f
   end
 
   definition BF_of_BG {n : ℕ} : BG n → BF n :=

homotopy/susp.hlean

@@ -0,0 +1,158 @@
+import ..pointed
+
+open susp eq pointed function is_equiv
+  variables {X X' Y Y' Z : Type*}
+
+-- move
+  definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) :=
+  pmap.mk ap1 (eq_of_phomotopy !ap1_pconst)
+
+  definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) :
+    ap1_gen (const A b) idp idp p = idp :=
+  ap1_gen_idp_left (const A b) p ⬝ ap_constant p b
+
+  definition ap1_gen_compose_const_left
+    {A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) :
+    ap1_gen_compose (const B c) f idp idp idp idp p ⬝
+    ap1_gen_const c (ap1_gen f idp idp p) =
+    ap1_gen_const c p :=
+  begin induction p, reflexivity end
+
+  definition ap1_gen_compose_const_right
+    {A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) :
+    ap1_gen_compose g (const A b) idp idp idp idp p ⬝
+    ap (ap1_gen g idp idp) (ap1_gen_const b p) =
+    ap1_gen_const (g b) p :=
+  begin induction p, reflexivity end
+
+  definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) :
+    phsquare (ap1_pcompose (pconst B C) f)
+             (ap1_pconst A C)
+             (ap1_phomotopy (pconst_pcompose f))
+             (pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) :=
+  begin
+    induction A with A a₀, induction B with B b₀, induction C with C c₀, induction f with f f₀,
+    esimp at *, induction f₀,
+    refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp,
+    fapply phomotopy_eq,
+    { exact ap1_gen_compose_const_left c₀ f },
+    { reflexivity }
+  end
+
+  definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) :
+    phsquare (ap1_pcompose g (pconst A B))
+             (ap1_pconst A C)
+             (ap1_phomotopy (pcompose_pconst g))
+             (pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) :=
+  begin
+    induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀,
+    esimp at *, induction g₀,
+    refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp,
+    fapply phomotopy_eq,
+    { exact ap1_gen_compose_const_right g b₀ },
+    { reflexivity }
+  end
+
+  definition pap1_natural_left [constructor] (f : X' →* X) :
+    psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) :=
+  begin
+    fapply phomotopy_mk_ppmap,
+    { intro g, exact !ap1_pcompose⁻¹* },
+    { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy  ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝
+      !phomotopy_of_eq_of_phomotopy)  ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾
+      idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ }
+  end
+
+  definition pap1_natural_right [constructor] (f : Y →* Y') :
+    psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) :=
+  begin
+    fapply phomotopy_mk_ppmap,
+    { intro g, exact !ap1_pcompose⁻¹* },
+    { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy  ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝
+      !phomotopy_of_eq_of_phomotopy)  ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾
+      idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ }
+  end
+
+namespace susp
+
+  definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : psusp X) :
+    psusp_functor (pconst X Y) x = pt :=
+  begin
+    induction x,
+    { reflexivity },
+    { exact (merid pt)⁻¹ },
+    { apply eq_pathover, refine !elim_merid ⬝ph _ ⬝hp !ap_constant⁻¹, exact square_of_eq !con.right_inv⁻¹ }
+  end
+
+  definition susp_functor_pconst [constructor] (X Y : Type*) : psusp_functor (pconst X Y) ~* pconst (psusp X) (psusp Y) :=
+  begin
+    fapply phomotopy.mk,
+    { exact susp_functor_pconst_homotopy },
+    { reflexivity }
+  end
+
+  definition psusp_pfunctor [constructor] (X Y : Type*) : ppmap X Y →* ppmap (psusp X) (psusp Y) :=
+  pmap.mk psusp_functor (eq_of_phomotopy !susp_functor_pconst)
+
+  definition psusp_pelim [constructor] (X Y : Type*) : ppmap X (Ω Y) →* ppmap (psusp X) Y :=
+  ppcompose_left (loop_psusp_counit Y) ∘* psusp_pfunctor X (Ω Y)
+
+  definition loop_psusp_pintro [constructor] (X Y : Type*) : ppmap (psusp X) Y →* ppmap X (Ω Y) :=
+  ppcompose_right (loop_psusp_unit X) ∘* pap1 (psusp X) Y
+
+  definition loop_psusp_pintro_natural_left (f : X' →* X) :
+    psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X' Y)
+            (ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
+  !pap1_natural_left ⬝h* ppcompose_right_psquare (loop_psusp_unit_natural f)⁻¹*
+
+  definition loop_psusp_pintro_natural_right (f : Y →* Y') :
+    psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X Y')
+            (ppcompose_left f) (ppcompose_left (Ω→ f)) :=
+  !pap1_natural_right ⬝h* !ppcompose_left_ppcompose_right⁻¹*
+
+  definition is_equiv_loop_psusp_pintro [constructor] (X Y : Type*) :
+    is_equiv (loop_psusp_pintro X Y) :=
+  begin
+    fapply adjointify,
+    { exact psusp_pelim X Y },
+    { intro g, apply eq_of_phomotopy, exact psusp_adjoint_loop_right_inv g },
+    { intro f, apply eq_of_phomotopy, exact psusp_adjoint_loop_left_inv f }
+  end
+
+  definition psusp_adjoint_loop' [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) :=
+  pequiv_of_pmap (loop_psusp_pintro X Y) (is_equiv_loop_psusp_pintro X Y)
+
+  definition psusp_adjoint_loop_natural_right (f : Y →* Y') :
+    psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X Y')
+            (ppcompose_left f) (ppcompose_left (Ω→ f)) :=
+  loop_psusp_pintro_natural_right f
+
+  definition psusp_adjoint_loop_natural_left (f : X' →* X) :
+    psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X' Y)
+            (ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
+  loop_psusp_pintro_natural_left f
+
+  definition iterate_psusp_iterate_psusp_rev (n m : ℕ) (A : Type*) :
+    iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (m + n) A :=
+  begin
+    induction n with n e,
+    { reflexivity },
+    { exact psusp_pequiv e }
+  end
+
+  definition iterate_psusp_pequiv [constructor] (n : ℕ) {X Y : Type*} (f : X ≃* Y) :
+    iterate_psusp n X ≃* iterate_psusp n Y :=
+  begin
+    induction n with n e,
+    { exact f },
+    { exact psusp_pequiv e }
+  end
+
+  open algebra nat
+  definition iterate_psusp_iterate_psusp (n m : ℕ) (A : Type*) :
+    iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (n + m) A :=
+  iterate_psusp_iterate_psusp_rev n m A ⬝e* pequiv_of_eq (ap (λk, iterate_psusp k A) (add.comm m n))
+
+end susp

known_bugs.txt

@@ -0,0 +1,28 @@
+- When using the "have" or "assert" tactic, no coercion is applied to the type. So you have to write for example
+`have g : Group.carrier G, from _,`
+instead of
+`have g : G, from _,`
+
+
+- When using the calc mode for homotopies, you have to give the proofs using a tactic (e.g. `by exact foo` instead of `foo`)
+
+- A file named "module.hlean" cannot be imported using `import .module` because `module` is a keyword (but it can be imported using `import ..foo.module`)
+
+Issues which are not bugs, but still good to know
+
+- once you start tactic mode, you cannot specify universe levels anymore
+
+- esimp is slow, and runs out of memory easily. It is good behavior to split up definitions. So instead of
+```
+equiv.MK (* big function *)
+         (* big inverse *)
+         (* long proof *)
+         (* long proof *)
+```
+first write the functions f and g and then write
+```
+equiv.MK f
+         g
+         abstract (* long proof *) end
+         abstract (* long proof *) end
+```

logic.hlean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2017 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad
+-/
+import types.trunc
+open funext eq trunc is_trunc prod sum
+
+--reserve prefix `¬`:40
+--reserve prefix `~`:40
+--reserve infixr ` ∧ `:35
+--reserve infixr ` /\ `:35
+--reserve infixr ` \/ `:30
+--reserve infixr ` ∨ `:30
+--reserve infix ` <-> `:20
+--reserve infix ` ↔ `:20
+
+namespace logic
+
+section
+open trunc_index
+
+definition propext {p q : Prop} (h : p ↔ q) : p = q :=
+tua (equiv_of_iff_of_is_prop h)
+
+end
+
+definition false : Prop := trunctype.mk empty _
+
+definition false.elim {A : Type} (h : false) : A := empty.elim h
+
+definition true : Prop := trunctype.mk unit _
+
+definition true.intro : true := unit.star
+
+definition trivial : true := unit.star
+
+definition and (p q : Prop) : Prop := tprod p q
+
+infixr ` ∧ ` := and
+infixr ` /\ ` := and
+
+definition and.intro {p q : Prop} (h₁ : p) (h₂ : q) : and p q := prod.mk h₁ h₂
+
+definition and.left {p q : Prop} (h : p ∧ q) : p := prod.pr1 h
+
+definition and.right {p q : Prop} (h : p ∧ q) : q := prod.pr2 h
+
+definition not (p : Prop) : Prop := trunctype.mk (p → empty) _
+
+prefix `~` := not
+
+definition or.inl := @or.intro_left
+
+definition or.inr := @or.intro_right
+
+end logic

move_to_lib.hlean

@@ -3,11 +3,29 @@
 import homotopy.sphere2 homotopy.cofiber homotopy.wedge
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     is_trunc function sphere unit sum prod
+     is_trunc function sphere unit sum prod bool
 
 definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
 !add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
 
+structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  ( im_in_ker : Π(a:A), g (f a) = pt)
+  ( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
+
+structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  ( im_in_ker : Π(a:A), g (f a) = pt)
+  ( ker_in_im : Π(b:B), (g b = pt) → image f b)
+
+definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
+is_exact f g
+
+definition is_exact_ag {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
+is_exact f g
+
+definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
+  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
+is_exact.mk H₁ H₂
+
 namespace algebra
   definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) :=
   by induction H; exact _
@@ -913,6 +931,14 @@ end category
 
 namespace sphere
 
+  definition psphere_pequiv_iterate_psusp (n : ℕ) : psphere n ≃* iterate_psusp n pbool :=
+  begin
+    induction n with n e,
+    { exact psphere_pequiv_pbool },
+    { exact psusp_pequiv e }
+  end
+
+
   -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
   --   f ~* pconst (S* n) (S* m) :=
   -- begin
@@ -968,14 +994,14 @@ begin
   exact ⦃ab_group, struct, mul_comm := H⦄
 end
 
-definition trivial_ab_group : AbGroup.{0} := 
+definition trivial_ab_group : AbGroup.{0} :=
 begin
   fapply AbGroup_of_Group Trivial_group, intro x y, reflexivity
 end
 
 definition trivial_homomorphism (A B : AbGroup) : A →g B :=
 begin
-  fapply homomorphism.mk, 
+  fapply homomorphism.mk,
   exact λ a, 1,
   intros, symmetry, exact one_mul 1,
 end
@@ -992,3 +1018,42 @@ definition is_embedding_from_trivial_ab_group (A : AbGroup) : is_embedding (from
 
 definition to_trivial_ab_group (A : AbGroup) : A →g trivial_ab_group :=
   trivial_homomorphism A trivial_ab_group
+
+/- Stuff added by Jeremy -/
+
+definition exists.elim {A : Type} {p : A → Type} {B : Type} [is_prop B] (H : Exists p)
+  (H' : ∀ (a : A), p a → B) : B :=
+trunc.elim (sigma.rec H') H
+
+definition image.elim {A B : Type} {f : A → B} {C : Type} [is_prop C] {b : B}
+  (H : image f b) (H' : ∀ (a : A), f a = b → C) : C :=
+begin
+  refine (trunc.elim _ H),
+  intro H'', cases H'' with a Ha, exact H' a Ha
+end
+
+definition image.intro {A B : Type} {f : A → B} {a : A} {b : B} (h : f a = b) : image f b :=
+begin
+  apply trunc.merely.intro,
+  apply fiber.mk,
+  exact h
+end
+
+definition image.equiv_exists {A B : Type} {f : A → B} {b : B} : image f b ≃ ∃ a, f a = b :=
+trunc_equiv_trunc _ (fiber.sigma_char _ _)
+
+-- move to homomorphism.hlean
+section
+  theorem eq_zero_of_eq_zero_of_is_embedding {A B : Type} [add_group A] [add_group B]
+    {f : A → B} [is_add_hom f] [is_embedding f] {a : A} (h : f a = 0) : a = 0 :=
+  have f a = f 0, by rewrite [h, respect_zero],
+  show a = 0, from is_injective_of_is_embedding this
+end
+
+/- put somewhere in algebra -/
+
+structure Ring :=
+(carrier : Type) (struct : ring carrier)
+
+attribute Ring.carrier [coercion]
+attribute Ring.struct [instance]

pointed.hlean

@@ -10,6 +10,10 @@ open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group si
 
 namespace pointed
 
+  definition loop_pequiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a')
+    : pointed.MK (a = a) idp ≃* pointed.MK (a' = a') idp :=
+  pequiv_of_equiv (loop_equiv_eq_closed p) (con.left_inv p)
+
   definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A :=
   begin
     fapply phomotopy.mk,
@@ -31,16 +35,16 @@ namespace pointed
   ap010 to_homotopy r a
 
   definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B}
-    {f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
-    (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') :
-      ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') =
-      whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') :=
+    {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
+    (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') (p : a = a') :
+      ap1_gen (λa, f a ⬝ f' a) (r₀ ◾ r₀') (r₁ ◾ r₁') p =
+      whisker_right q₀' (ap1_gen f r₀ r₁ p) ⬝ whisker_left q₁ (ap1_gen f' r₀' r₁' p) :=
   begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end
 
   definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B}
     {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂}
     (r₀ : f a = q₀) (r₁ : f' a = q₁) :
-      ap1_gen_con_left idp r₀ r₀ r₁ r₁ =
+      ap1_gen_con_left r₀ r₀ r₁ r₁ idp =
       !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ :=
   begin induction r₀, induction r₁, reflexivity end
 
@@ -138,6 +142,10 @@ namespace pointed
   postfix `⁻¹ʰ*`:(max+1) := phinverse
   postfix `⁻¹ᵛ*`:(max+1) := pvinverse
 
+  definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ :=
+  !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc
+
   definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
     psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) :=
   !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
@@ -402,6 +410,22 @@ namespace pointed
     {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* :=
   !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
 
+  definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+    {r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q :=
+  !refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
+
+  definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+    {r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q :=
+  idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans
+
+  definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+    {r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q :=
+  !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
+
+  definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+    {r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p :=
+  s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl
+
   section phsquare
   /-
     Squares of pointed homotopies
@@ -421,6 +445,17 @@ namespace pointed
   definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p
   definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p
 
+  -- definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x))
+  --   (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂))
+  --             (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁))
+  --             (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ :=
+  -- begin
+  --   fapply phomotopy_eq,
+  --   { intro x, apply eq_of_square (p x) },
+  --   { generalize p pt, intro r, exact sorry }
+  -- end
+
+
   definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) :
     phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ :=
   !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc
@@ -495,6 +530,10 @@ namespace pointed
     (q : phsquare p₁₀ p₁₂ (p ⬝* p₀₁) p₂₁) : phsquare (p⁻¹* ⬝* p₁₀) p₁₂ p₀₁ p₂₁ :=
   !trans_assoc ⬝ (eq_symm_trans_of_trans_eq (q ⬝ !trans_assoc)⁻¹)⁻¹
 
+  definition phmove_bot_of_left {p₀₁ : f₀₀ ~* f} (p : f ~* f₀₂)
+    (q : phsquare p₁₀ p₁₂ (p₀₁ ⬝* p) p₂₁) : phsquare p₁₀ (p ⬝* p₁₂) p₀₁ p₂₁ :=
+  q ⬝ !trans_assoc
+
   definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B}
     (p : f ~* f') : phsquare (passoc h g f) (passoc h g f')
       (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) :=
@@ -557,6 +596,37 @@ namespace pointed
     exact !pwhisker_right_refl⁻¹
   end
 
+  definition phomotopy_of_eq_pcompose_left {A B C : Type*} (g : B →* C) {f f' : A →* B}
+    (p : f = f') : phomotopy_of_eq (ap (λf, g ∘* f) p) = pwhisker_left g (phomotopy_of_eq p) :=
+  begin
+    induction p, exact !pwhisker_left_refl⁻¹
+  end
+
+  definition phomotopy_of_eq_pcompose_right {A B C : Type*} {g g' : B →* C} (f : A →* B)
+    (p : g = g') : phomotopy_of_eq (ap (λg, g ∘* f) p) = pwhisker_right f (phomotopy_of_eq p) :=
+  begin
+    induction p, exact !pwhisker_right_refl⁻¹
+  end
+
+  definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) :
+    ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) :=
+  begin
+    -- induction X with X x₀, induction Y with Y y₀, induction f with f f₀, esimp at *, induction f₀,
+    -- fapply phomotopy_eq,
+    -- { intro x, unfold [ap1_phomotopy], },
+    -- { }
+    exact sorry
+  end
+
+  definition ap1_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
+    ap Ω→ (eq_of_phomotopy p) = eq_of_phomotopy (ap1_phomotopy p) :=
+  begin
+    induction p using phomotopy_rec_on_idp,
+    refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
+    exact !ap1_phomotopy_refl⁻¹
+  end
+
+  -- duplicate of ap_eq_of_phomotopy
   definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
     ap010 pmap.to_fun (eq_of_phomotopy p) a = p a :=
   begin
@@ -606,23 +676,43 @@ namespace pointed
     pwhisker_right f (pcompose_pconst g) ⬝* pconst_pcompose f :=
   begin
     fapply phomotopy_eq,
-    { intro a, esimp, exact !idp_con ⬝ !idp_con },
+    { intro a, exact !idp_con ⬝ !idp_con },
     { induction g with g g₀, induction f with f f₀, induction B' with D d₀, induction A with C c₀,
       esimp at *, induction g₀, induction f₀, reflexivity }
   end
 
+  definition passoc_pconst_left {A B C D : Type*} (g : B →* C) (f : A →* B) :
+    phsquare (passoc (pconst C D) g f) (pconst_pcompose f)
+             (pwhisker_right f (pconst_pcompose g)) (pconst_pcompose (g ∘* f)) :=
+  begin
+    fapply phomotopy_eq,
+    { intro a, exact !idp_con },
+    { induction g with g g₀, induction f with f f₀, induction C with C c₀, induction B with B b₀,
+      esimp at *, induction g₀, induction f₀, reflexivity }
+  end
+
   definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) :
     @ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g :=
   begin
     fapply phomotopy_mk_ppmap,
     { exact passoc h g },
-    { esimp,
-      refine idp ◾** (!phomotopy_of_eq_con ⬝
+    { refine idp ◾** (!phomotopy_of_eq_con ⬝
         (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
         !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
       exact passoc_pconst_right h g }
   end
 
+  definition ppcompose_right_pcompose [constructor] {A B C D : Type*} (g : B →* C) (f : A →* B) :
+    @ppcompose_right _ _ D (g ∘* f) ~* ppcompose_right f ∘* ppcompose_right g :=
+  begin
+    symmetry,
+    fapply phomotopy_mk_ppmap,
+    { intro h, exact passoc h g f },
+    { refine idp ◾** !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝
+        (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+      exact passoc_pconst_left g f }
+  end
+
   definition ppcompose_left_ppcompose_right {A A' B B' : Type*} (g : B →* B') (f : A' →* A) :
     psquare (ppcompose_left g) (ppcompose_left g) (ppcompose_right f) (ppcompose_right f) :=
   begin
@@ -674,6 +764,16 @@ namespace pointed
     reflexivity
   end
 
+  definition ppcompose_right_phomotopy [constructor] {A B C : Type*} {f f' : A →* B} (p : f ~* f') :
+    @ppcompose_right _ _ C f ~* ppcompose_right f' :=
+  begin
+    induction p using phomotopy_rec_on_idp,
+    reflexivity
+  end
+
+  definition pppcompose [constructor] (A B C : Type*) : ppmap B C →* ppmap (ppmap A B) (ppmap A C) :=
+  pmap.mk ppcompose_left (eq_of_phomotopy !ppcompose_left_pconst)
+
   section psquare
 
   variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
@@ -688,6 +788,11 @@ namespace pointed
             (ppcompose_left f₀₁) (ppcompose_left f₂₁) :=
   !ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose
 
+  definition ppcompose_right_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare (@ppcompose_right _ _ A f₁₂) (ppcompose_right f₁₀)
+            (ppcompose_right f₂₁) (ppcompose_right f₀₁) :=
+  !ppcompose_right_pcompose⁻¹* ⬝* ppcompose_right_phomotopy p⁻¹* ⬝* !ppcompose_right_pcompose
+
   definition trans_phomotopy_hconcat {f₀₁' f₀₁''}
     (q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
     (q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p :=
@@ -782,23 +887,97 @@ namespace pointed
     pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
   ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
 
-  definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
+  definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
+  (loop_pmap_commute X Y)⁻¹ᵉ*
+
+  definition loop_phomotopy [constructor] {A B : Type*} (f : A →* B) : Type* :=
+  pointed.MK (f ~* f) phomotopy.rfl
+
+  definition ppcompose_left_loop_phomotopy [constructor] {A B C : Type*} (g : B →* C) {f : A →* B}
+    {h : A →* C} (p : g ∘* f ~* h) : loop_phomotopy f →* loop_phomotopy h :=
+  pmap.mk (λq, p⁻¹* ⬝* pwhisker_left g q ⬝* p)
+    (idp ◾** !pwhisker_left_refl ◾** idp ⬝ !trans_refl ◾** idp ⬝ !trans_left_inv)
+
+  definition ppcompose_left_loop_phomotopy' [constructor] {A B C : Type*} (g : B →* C) (f : A →* B)
+    : loop_phomotopy f →* loop_phomotopy (g ∘* f) :=
+  pmap.mk (λq, pwhisker_left g q) !pwhisker_left_refl
+
+  definition ppcompose_left_loop_phomotopy_refl {A B C : Type*} (g : B →* C) (f : A →* B)
+    : ppcompose_left_loop_phomotopy g phomotopy.rfl ~* ppcompose_left_loop_phomotopy' g f :=
+  phomotopy.mk (λq, !refl_symm ◾** idp ◾** idp ⬝ !refl_trans ◾** idp ⬝ !trans_refl)
+    begin
+      esimp, exact sorry
+    end
+
+  definition loop_ppmap_pequiv' [constructor] (A B : Type*) :
+    Ω(ppmap A B) ≃* loop_phomotopy (pconst A B) :=
+  pequiv_of_equiv (pmap_eq_equiv _ _) idp
+
+  -- definition loop_ppmap (A B : Type*) : pointed.MK (pconst A B ~* pconst A B) phomotopy.rfl ≃*
+  --   pointed.MK (Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl) ⟨homotopy.rfl, idp⟩ :=
+  -- pequiv_of_equiv !phomotopy.sigma_char _
+
+  definition ppmap_loop_pequiv' [constructor] (A B : Type*) :
+    loop_phomotopy (pconst A B) ≃* ppmap A (Ω B) :=
+  pequiv_of_equiv (!phomotopy.sigma_char ⬝e !pmap.sigma_char⁻¹ᵉ) idp
+
+  definition loop_ppmap_pequiv [constructor] (A B : Type*) : Ω(ppmap A B) ≃* ppmap A (Ω B) :=
+  loop_ppmap_pequiv' A B ⬝e* ppmap_loop_pequiv' A B
+
+  definition loop_ppmap_pequiv'_natural_right' {X X' : Type} (x₀ : X) (A : Type*) (f : X → X') :
+    psquare (loop_ppmap_pequiv' A _) (loop_ppmap_pequiv' A _)
+            (Ω→ (ppcompose_left (pmap_of_map f x₀)))
+            (ppcompose_left_loop_phomotopy' (pmap_of_map f x₀) !pconst) :=
   begin
-    fapply pequiv_of_equiv,
-    { fapply equiv.MK: esimp,
-      { intro f, fapply pmap_eq,
-        { intro x, exact f x },
-        { exact (respect_pt f)⁻¹ }},
-      { intro p, fapply pmap.mk,
-        { intro x, exact ap010 pmap.to_fun p x },
-        { note z := apd respect_pt p,
-          note z2 := square_of_pathover z,
-          refine eq_of_hdeg_square z2 ⬝ !ap_constant }},
-      { intro p, exact sorry },
-      { intro p, exact sorry }},
-    { apply pmap_eq_idp}
+    fapply phomotopy.mk,
+    { esimp, intro p,
+     refine _ ⬝ ap011 (λx y, phomotopy_of_eq (ap1_gen _ x y _))
+                 proof !eq_of_phomotopy_refl⁻¹ qed proof !eq_of_phomotopy_refl⁻¹ qed,
+     refine _ ⬝ ap phomotopy_of_eq !ap1_gen_idp_left⁻¹,
+     exact !phomotopy_of_eq_pcompose_left⁻¹ },
+    { refine _ ⬝ !idp_con⁻¹, exact sorry }
   end
 
+  definition loop_ppmap_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (loop_ppmap_pequiv' A X) (loop_ppmap_pequiv' A X')
+            (Ω→ (ppcompose_left f)) (ppcompose_left_loop_phomotopy f !pcompose_pconst) :=
+  begin
+    induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀,
+    apply psquare_of_phomotopy,
+    exact sorry
+    -- fapply phomotopy.mk,
+    -- { esimp, esimp [pmap_eq_equiv], intro p, },
+    -- { }
+  end
+
+  definition ppmap_loop_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (ppmap_loop_pequiv' A X) (ppmap_loop_pequiv' A X')
+            (ppcompose_left_loop_phomotopy f !pcompose_pconst) (ppcompose_left (Ω→ f)) :=
+  begin
+    exact sorry
+  end
+
+  definition loop_pmap_commute_natural_right_direct {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (loop_ppmap_pequiv A X) (loop_ppmap_pequiv A X')
+            (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
+  begin
+    induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀,
+--    refine _ ⬝* _ ◾* _, rotate 4,
+    fapply phomotopy.mk,
+    { intro p, esimp, esimp [pmap_eq_equiv, pcompose_pconst], exact sorry },
+    { exact sorry }
+  end
+
+  definition loop_pmap_commute_natural_left {A A' : Type*} (X : Type*) (f : A' →* A) :
+    psquare (loop_pmap_commute A X) (loop_pmap_commute A' X)
+            (Ω→ (ppcompose_right f)) (ppcompose_right f) :=
+  sorry
+
+  definition loop_pmap_commute_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (loop_pmap_commute A X) (loop_pmap_commute A X')
+            (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
+  loop_ppmap_pequiv'_natural_right A f ⬝h* ppmap_loop_pequiv'_natural_right A f
+
   /-
     Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine?
     If we set up things more generally, we could define this as
@@ -806,7 +985,8 @@ namespace pointed
   -/
   structure phomotopy2 {A B : Type*} {f g : A →* B} (p q : f ~* g) : Type :=
     (homotopy_eq : p ~ q)
-    (homotopy_pt_eq : whisker_right (respect_pt g) (homotopy_eq pt) ⬝ to_homotopy_pt q = to_homotopy_pt p)
+    (homotopy_pt_eq : whisker_right (respect_pt g) (homotopy_eq pt) ⬝ to_homotopy_pt q =
+      to_homotopy_pt p)
 
   /- this sets it up more generally, for illustrative purposes -/
   structure ppi' (A : Type*) (P : A → Type) (p : P pt) :=
@@ -815,12 +995,13 @@ namespace pointed
   attribute ppi'.to_fun [coercion]
   definition ppi_homotopy' {A : Type*} {P : A → Type} {x : P pt} (f g : ppi' A P x) : Type :=
   ppi' A (λa, f a = g a) (ppi'.resp_pt f ⬝ (ppi'.resp_pt g)⁻¹)
-  definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x} (p q : ppi_homotopy' f g) : Type :=
+  definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x}
+    (p q : ppi_homotopy' f g) : Type :=
   ppi_homotopy' p q
 
-  infix ` ~*2 `:50 := phomotopy2
+  -- infix ` ~*2 `:50 := phomotopy2
 
-  variables {A B : Type*} {f g : A →* B} (p q : f ~* g)
+  -- variables {A B : Type*} {f g : A →* B} (p q : f ~* g)
 
   -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
   -- sorry

set.hlean

@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2017 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad
+-/
+import types.trunc .logic
+open funext eq trunc is_trunc logic
+
+definition set (X : Type) := X → Prop
+
+namespace set
+
+variable {X : Type}
+
+/- membership and subset -/
+
+definition mem (x : X) (a : set X) := a x
+infix ∈ := mem
+notation a ∉ b := ¬ mem a b
+
+theorem ext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b :=
+eq_of_homotopy (take x, propext (H x))
+
+definition subset (a b : set X) : Prop := Prop.mk (∀⦃x⦄, x ∈ a → x ∈ b) _
+infix ⊆ := subset
+
+definition superset (s t : set X) : Prop := t ⊆ s
+infix ⊇ := superset
+
+theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
+
+theorem subset.trans {a b c : set X} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
+take x, assume ax, subbc (subab ax)
+
+theorem subset.antisymm {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
+ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb))
+
+-- an alterantive name
+theorem eq_of_subset_of_subset {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
+subset.antisymm h₁ h₂
+
+theorem mem_of_subset_of_mem {s₁ s₂ : set X} {a : X} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
+assume h₁ h₂, h₁ _ h₂
+
+/- empty set -/
+
+definition empty : set X := λx, false
+notation `∅` := empty
+
+theorem not_mem_empty (x : X) : ¬ (x ∈ ∅) :=
+assume H : x ∈ ∅, H
+
+theorem mem_empty_eq (x : X) : x ∈ ∅ = false := rfl
+
+theorem eq_empty_of_forall_not_mem {s : set X} (H : ∀ x, x ∉ s) : s = ∅ :=
+ext (take x, iff.intro
+  (assume xs, absurd xs (H x))
+  (assume xe, absurd xe (not_mem_empty x)))
+
+theorem ne_empty_of_mem {s : set X} {x : X} (H : x ∈ s) : s ≠ ∅ :=
+  begin intro Hs, rewrite Hs at H, apply not_mem_empty x H end
+
+theorem empty_subset (s : set X) : ∅ ⊆ s :=
+take x, assume H, empty.elim H
+
+theorem eq_empty_of_subset_empty {s : set X} (H : s ⊆ ∅) : s = ∅ :=
+subset.antisymm H (empty_subset s)
+
+theorem subset_empty_iff (s : set X) : s ⊆ ∅ ↔ s = ∅ :=
+iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
+
+/- universal set -/
+
+definition univ : set X := λx, true
+
+theorem mem_univ (x : X) : x ∈ univ := trivial
+
+theorem mem_univ_eq (x : X) : x ∈ univ = true := rfl
+
+theorem empty_ne_univ [h : inhabited X] : (empty : set X) ≠ univ :=
+assume H : empty = univ,
+absurd (mem_univ (inhabited.value h)) (eq.rec_on H (not_mem_empty (arbitrary X)))
+
+theorem subset_univ (s : set X) : s ⊆ univ := λ x H, unit.star
+
+theorem eq_univ_of_univ_subset {s : set X} (H : univ ⊆ s) : s = univ :=
+eq_of_subset_of_subset (subset_univ s) H
+
+theorem eq_univ_of_forall {s : set X} (H : ∀ x, x ∈ s) : s = univ :=
+ext (take x, iff.intro (assume H', unit.star) (assume H', H x))
+
+
+
+/- set-builder notation -/
+
+-- {x : X | P}
+definition set_of (P : X → Prop) : set X := P
+notation `{` binder ` | ` r:(scoped:1 P, set_of P) `}` := r
+
+-- {x ∈ s | P}
+definition sep (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
+notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r
+
+/- insert -/
+
+definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
+
+-- '{x, y, z}
+notation `'{`:max a:(foldr `, ` (x b, insert x b) ∅) `}`:0 := a
+
+theorem subset_insert (x : X) (a : set X) : a ⊆ insert x a :=
+take y, assume ys, or.inr ys
+
+theorem mem_insert (x : X) (s : set X) : x ∈ insert x s :=
+or.inl rfl
+
+theorem mem_insert_of_mem {x : X} {s : set X} (y : X) : x ∈ s → x ∈ insert y s :=
+assume h, or.inr h
+
+theorem eq_or_mem_of_mem_insert {x a : X} {s : set X} : x ∈ insert a s → x = a ∨ x ∈ s :=
+assume h, h
+
+end set