From 9cf51e98cdeeac96d73624e2d77398b81c488086 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 8 Mar 2017 21:30:38 -0500 Subject: [PATCH] start on notes --- Notes/smash.tex | 175 ++++++++++++++++++++++++++++++++++++++++++ homotopy/smash.hlean | 57 ++++++++++++-- homotopy/smash2.hlean | 116 ++++++++++++++++++++++++++++ pointed.hlean | 40 +++++++++- 4 files changed, 377 insertions(+), 11 deletions(-) create mode 100644 Notes/smash.tex create mode 100644 homotopy/smash2.hlean diff --git a/Notes/smash.tex b/Notes/smash.tex new file mode 100644 index 0000000..47402f9 --- /dev/null +++ b/Notes/smash.tex @@ -0,0 +1,175 @@ +\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}} + +\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 (and higher cells) we take equalities between pointed homotopies. +\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, but since the + aforementioned equivalence requires function extensionality, it is better to define the type of + pointed homotopies manually in a type theory where function extensionality doesn't compute (like + Lean). 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$. In these + notes we will not use $0$ for the empty type (since that is not pointed, we will not use the empty + type). +\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{lem}\mbox{} + \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: + $(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 $f\smash0\sim0$ and $0\smash g\sim 0$. + \end{itemize} +\end{lem} + +\begin{lem} + 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 $g_1$ or $g_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. +\end{lem} +\begin{proof} +We will only do the case where $g_1\jdeq 0$, the other case is similar (but slightly easier). In this case, we need to show that the following diagram commutes. +\begin{center} +\begin{tikzcd} +(f_2 \o f_1)\smash (g_2 \o 0) \arrow[r, equals]\arrow[dd,equals] & +(f_2 \smash g_1)\o (f_1 \o 0)\arrow[d,equals] \\ +& (f_2 \smash g_1)\o 0\arrow[d,equals] \\ +(f_2 \o f_1)\smash 0 \arrow[r,equals] & +0 +\end{tikzcd} +\end{center} +Proof to do. +\end{proof} + +\begin{thm}\label{thm:smash-functor-right} +Given pointed types $A$, $A'$ and $B$, the functorial action of the smash product induces a map +$$({-})\smash B:(A\pmap A')\pmap(A\smash B\pmap A'\smash B)$$ +which is natural in $A$, $A'$ and $B$. (note: it's both covariant and contravariant in $B$). +\end{thm} +\begin{proof} +First note that $\lam{f}f\smash B$ preserves the basepoint so that the map is indeed pointed. +\end{proof} + +\section{Adjunction} + +\begin{defn} +There is a unit $\eta:A\pmap B\pmap A\smash B$ and counit $\epsilon : (B\pmap C)\smash B \pmap C$ +\end{defn} + + +\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)).$$ + +\begin{lem} +$e$ has an inverse $\inv e\jdeq \inv{e}_{A,B,C}:(A\smash B\pmap C)\pmap(A\pmap B\pmap C)$ which is defined as +$$(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).$$ +\begin{proof} +We do not actually use that $\inv{e}_{A,B,C}$ has this form in later proofs, we only use that $e$ is invertible (the former fact is also not formalized). Proof to do. +\end{proof} +\end{lem} +\end{defn} +\begin{lem} +$e$ is natural in $A$, $B$ and $C$. +\end{lem} +\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} + + +\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} diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index cbe1dcc..b9ee092 100644 --- a/homotopy/smash.hlean +++ b/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) : @@ -446,10 +457,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 := @@ -548,10 +567,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,6 +650,30 @@ namespace smash rexact H (gluel (f' (f a₀))) } end + /- 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_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 _⁻¹*, + 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 + /- a lemma using both these rules -/ definition smash_psquare_lemma (f : A →* A') (g : B →* B') diff --git a/homotopy/smash2.hlean b/homotopy/smash2.hlean new file mode 100644 index 0000000..8826fc7 --- /dev/null +++ b/homotopy/smash2.hlean @@ -0,0 +1,116 @@ +import .smash_adjoint + +-- Authors: Floris van Doorn + +import homotopy.smash ..pointed .pushout homotopy.red_susp + +open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc + function red_susp unit + + /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (?) (notation means suspension, wedge, smash) -/ + + /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/ + + /- To prove: A ∧ S¹ ≃ ΣA -/ + + /- associativity is proven in smash_adjoint -/ +variables {A A' B B' C C' D E F : Type*} + +namespace smash + + definition smash_pelim2 [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C := + ppcompose_left (smash_pmap_counit B C) ∘* smash_functor_right B A (ppmap B C) + + definition smash_pelim2_natural (f : C →* C') : + psquare (smash_pelim2 A B C) (smash_pelim2 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 f) + +--ppmap B C →* ppmap (A ∧ B) (A ∧ C) + 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_lemma (f : A →* A') + : phsquare (smash_functor_psquare (phomotopy.rfl : psquare f f !pid !pid) + (phomotopy.rfl : psquare !pid !pid (pconst B C) (pconst B C))) + (pconst_pcompose (f ∧→ pid B)) + (pwhisker_right (f ∧→ pid B) (smash_functor_pconst_right (pid A'))) + (pwhisker_right (f ∧→ pid B) (smash_functor_pconst_right (pid A')) ⬝* + pconst_pcompose (f ∧→ pid B)) := + 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 + 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 smash_functor_pid_pcompose_pconst + +} + end + + definition smash_pelim2_natural_left (B C : Type*) (f : A' →* A) : + psquare (smash_pelim2 A B C) (smash_pelim2 A' B C) + (ppcompose_right f) (ppcompose_right (pid B ∧→ f)) := + smash_functor_right_natural_middle f ⬝h* !ppcompose_left_ppcompose_right + + definition smash_pelim2_natural_middle (A C : Type*) (g : B' →* B) : + psquare (smash_pelim2 A B C) (smash_pelim2 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_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 + + definition smash_pelim2_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) : + psquare (smash_pelim2 A B C) (smash_pelim2 A' B' C) + (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (g ∧→ f)) := + smash_pelim2_natural_left B C f ⬝v* smash_pelim2_natural_middle A' C g ⬝hp* + ppcompose_right_phomotopy proof !smash_functor_split qed ⬝* !ppcompose_right_pcompose + +end smash diff --git a/pointed.hlean b/pointed.hlean index 784bf17..6c7d25e 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -138,6 +138,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 @@ -606,23 +610,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 +698,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*}